User loginNavigation 
Nonstandard type theories for FPGiven the recent discussion in the Subtyping+overloading thread I wanted to ask a question which has been bugging me (for ages). I assume we all known HM style type inference. As I understand it, HM has been extended with quantifiers to allow multiple instantiations of the same type, or hiding of known types. I.e., the following good old example only type checks if 'id' has type 'forall a. a > a': let id = \x . x in (id true, id 1) Great, problem solved, one would think. My problem with the current definition of the quantifiers is the following. A bold statement: the types (1) 'forall a . a' and (2) 'forall a b . a > b' should not exist! I find it strange for (1) that a term can be written which unifies with any given type, similar in case (2), where a result is produced which can get any type. Let me define the predicate 'great!' as types I personally like. A type 'forall a . a > a' is 'great!' since you know that the first 'a' will be bound by an argument, and a term can then be generated which holds the same type. A type '(forall a . a) > (exists b . b)' is also 'great!' since it takes a known type, and produces a value out of a hidden type. I am wondering if the current quantifiers were too much inspired by HM [or type theory], and are a false solution to the multiple instantiation problem. So I am looking for nonstandard approaches which tackle this. By marco at 20081124 07:52  LtU Forum  previous forum topic  next forum topic  other blogs  10004 reads

Browse archives
Active forum topics

Recent comments
19 weeks 6 days ago
24 weeks 1 day ago
25 weeks 5 days ago
25 weeks 5 days ago
28 weeks 3 days ago
33 weeks 15 hours ago
33 weeks 17 hours ago
33 weeks 3 days ago
33 weeks 3 days ago
36 weeks 2 days ago