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

Browse archivesActive forum topics 
Recent comments
7 min 37 sec ago
4 hours 13 min ago
5 hours 12 min ago
6 hours 39 min ago
6 hours 51 min ago
7 hours 43 min ago
9 hours 18 min ago
10 hours 53 min ago
11 hours 10 min ago
17 hours 31 min ago