Polymorphic recursion

[AshleyYakeley]

Infer type of let rec f = seq (f 3) end in f Expected: a -> a Found: a -> (a | Integer). This type is sound, but is not the principal type.

[AshleyYakeley]

Consider:

fixf = fn f => let rec x = f x end in x;
rf = fn r => seq (r 3);
rr = fixf rf;

Inferred types:

• fixf: (a -> a) -> a
• rf: (Integer -> Any) -> a -> a
• rr: a -> (a | Integer)

These inferences are correct.

[AshleyYakeley]

The key code is this:

data AbstractResult ts a =
    forall t. MkAbstractResult (TSNegWitness ts t)
                               (UnifierExpression ts (t -> a))

abstractResult ::
       forall ts a. AbstractTypeSystem ts
    => TSVarID ts
    -> TSOpenExpression ts a
    -> TSOuter ts (AbstractResult ts a)

This is correct when used for lambda abstractions, where the type of the function domain is negative. But it's incorrect when used for recursive lets, where the types of all bindings are positive.

[AshleyYakeley]

let f = ... f ... f ... f in f

Need to calculate a positive type T that subsumes to all of T1, T2, T3 etc.

[AshleyYakeley]

Simple approach: given negative type Ta from abstraction and positive type Tr from value, find best positive type T such that:

• T <: Ta
• Tr <: T

Example: rf: (Integer -> Any) -> a -> a

• Tr = a -> a
• Ta = Integer -> Any
• gives T = a -> a

[AshleyYakeley]

• T+ <: Ta-
• Tr+ <: T+ same as
• Ta -> Tr + <: T -> T + ?

No, because

• (Integer -> Any) -> a -> a <: (a -> a) -> a -> a
• (Integer -> Any) -> a -> a <: (a -> a) -> b -> b

both fail.

[AshleyYakeley]

Wait, just pick T = Tr.

[AshleyYakeley]

r = let x = Just x in x;
f = fn x => Just x;

gives

• Tr+ = Maybe a
• Ta- = a
• Ta -> Tr + = a -> Maybe a

[AshleyYakeley]

• (Integer -> Any) -> a -> a => a -> a
• a -> Maybe a => rec a, Maybe a
• Any -> Integer => Integer
• Maybe Integer -> Maybe None => Maybe None
• ((Text | Integer) -> Any) -> a -> a => a -> a

[AshleyYakeley]

• let rec v = fn x => seq (v 3) $ seq (v "t") x end in v
• fn v => fn x => seq (v 3) $ seq (v "t") x has type ((Text | Integer) -> Any) -> a -> a

[AshleyYakeley]

Test: let rec f: T = f end; rec v = f v end in v

[AshleyYakeley]

Inverse subsumption P- -> Q+ (rigid) to a- -> a+ (free)?

[AshleyYakeley]

Apparently polymorphic recursion inference isn't decideable (LPTK/simple-sub#94), and we can already do it with type signatures, so we won't be doing this.

[AshleyYakeley]

This doesn't seem to be working even with type signatures.

[AshleyYakeley]

OK, this is fixed now.