03 Polymorphism, subtyping, and ytpe inference in MLsub

…map :: forall a b. a -> b -> [a -> b] mapmap = map @(a -> b) @(a -> b) $ map @a @b We can type, etc. selfId :: (forall xx. xx -> xx) -> (forall a. a -> a) selfId id = id id ---- The inferred type in the **MLsub** type system (which has type inference with subtyping + ^\(*parametric*\) polymorphism) is ^\(link to this video, ^interactive\) self :: (a -> b) & a -> b self x = x x and applying `self` to itself gives a bottom type omega :: Bot omega = self self and lets us type the Y-combinator y :: (a -> a) -> a y t = (\x -> t (x x)) (\x -> t (x x))…

Polymorphism, subtyping, and type inference in MLsub (Stephen Dolan, ML workshop 2015)

I didn't mention any paper, but thanks for pointing out that there is one! I found the ICFP 2015 presentation of the paper short, entertaining, and enlightening. I can now answer my own questions: > Could you summarize what's algebraic subtyping? Add union types `a ⊔ b` and intersection types `a ⊓ b`, with subtyping rules `a ≤ a ⊔ b`, `b ≤ a ⊔ b`, `a ⊓ b ≤ a`, and `a ⊓ b ≤ b`. Restrict those new types so that only input types can use `⊓` and only output types can use `⊔`, and tada! Inference becomes easy, even if you throw in parametric polymorphism. The restriction doesn't unduly restrict expressibility because it is input values which can be used in both an `a` way and a `b` way (thus…