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  10188 reads

Browse archives
Active forum topics 
Recent comments
12 weeks 3 days ago
12 weeks 3 days ago
12 weeks 3 days ago
34 weeks 4 days ago
38 weeks 6 days ago
40 weeks 4 days ago
40 weeks 4 days ago
43 weeks 1 day ago
47 weeks 6 days ago
47 weeks 6 days ago