[kvb]

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]

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/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]

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]

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).