7 ms·

Though note that an even better type would probably be twice : forall a,b,c. ((a->b)&(b->c)) -> a -> c (e.g. in MLSub, the type for twice (fun x -> x

by kvb 10y ago

Though note that an even better type would probably be twice : forall a,b,c. ((a->b)&(b->c)) -> a -> c (e.g. in MLSub, the type for twice (fun x -> x::[]) 1 is the unsatisfying (rec a = (a list | int) list) rather than the expected (int list) list )

tomp 10y ago
You're right, interesting example! Although I'd prefer to "fix" this by incorporating first-class polymorphism [1] with MLsub - I guess non-polymorphic functions satisfying the constraint `(a -> b) & (b -> c)` are quite rare (although I'm sure that you can think of an example). [1] https://github.com/tomprimozic/type-systems/tree/master/first_class_polymorphism https://github.com/tomprimozic/type-systems/tree/master/firs... Edit: although on second thought, just first-class polymorphism isn't enough to fix this... any type system where the function `twice` has the same type as the function `three_times` will exhibit the same problem!
- kvb 10y ago
  Non-polymorphic functions of the type `a->a` trivially satisfy it, of course. Also, I think polymorphic functions are the most interesting case where you can't use twice as desired in an ML-like language, so it's too bad that despite the fancier type they don't work too well in MLsub. Here's another example that fails when I'd hope for it to succeed: let one = twice (fun o -> o.x) { x = { x = 1 } }
Jweb_Guru 10y ago
It seems that if you try to ascribe the type you wrote to twice you do get (a -> (a & b)) -> a -> b. I suspect this is a direct result of the "extensional" principles used to design the subtyping relation (so that it forms a lattice with nice properties) and I'm not sure whether it would be at all easy to get around. But I could be wrong, I'm still digesting the paper. (Actually, I think it conceivably might just be a bug in the current typechecker; ascription isn't working for records AFAICT which makes me think they might not be fully baked).

by kvb 10y ago

tomp 10y ago

You're right, interesting example! Although I'd prefer to "fix" this by incorporating first-class polymorphism [1] with MLsub - I guess non-polymorphic functions satisfying the constraint `(a -> b) & (b -> c)` are quite rare (although I'm sure that you can think of an example). [1] https://github.com/tomprimozic/type-systems/tree/master/first_class_polymorphism https://github.com/tomprimozic/type-systems/tree/master/firs... Edit: although on second thought, just first-class polymorphism isn't enough to fix this... any type system where the function `twice` has the same type as the function `three_times` will exhibit the same problem!

kvb 10y ago
Non-polymorphic functions of the type `a->a` trivially satisfy it, of course. Also, I think polymorphic functions are the most interesting case where you can't use twice as desired in an ML-like language, so it's too bad that despite the fancier type they don't work too well in MLsub. Here's another example that fails when I'd hope for it to succeed: let one = twice (fun o -> o.x) { x = { x = 1 } }

Jweb_Guru 10y ago

It seems that if you try to ascribe the type you wrote to twice you do get (a -> (a & b)) -> a -> b. I suspect this is a direct result of the "extensional" principles used to design the subtyping relation (so that it forms a lattice with nice properties) and I'm not sure whether it would be at all easy to get around. But I could be wrong, I'm still digesting the paper. (Actually, I think it conceivably might just be a bug in the current typechecker; ascription isn't working for records AFAICT which makes me think they might not be fully baked).