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

Browse archivesActive forum topics 
Recent comments
18 hours 27 min ago
21 hours 6 min ago
1 day 16 hours ago
1 day 23 hours ago
2 days 2 hours ago
2 days 3 hours ago
2 days 5 hours ago
2 days 21 hours ago
3 days 1 hour ago
6 days 8 hours ago