hkust-taco / mlscript

The MLscript programming language. Functional and object-oriented; structurally typed and sound; with powerful type inference. Soon to have full interop with TypeScript!
https://hkust-taco.github.io/mlscript
MIT License
175 stars 27 forks source link

Some generic object types are not lattice homomorphisms and those which are should not be forall-distributivity targets #207

Open LPTK opened 10 months ago

LPTK commented 10 months ago

We currently allow defining generic modules, as in:

module Test[A] {
  fun foo: A -> A = id
}
//│ module Test[A] {
//│   fun foo: A -> A
//│ }

Test
//│ forall 'A. Test['A]
//│ res
//│     = Test { class: [class Test] }

Test.foo
//│ 'A -> 'A
//│ res
//│     = [Function: id]

Test.foo(1) + 1
//│ Int
//│ res
//│     = 2

not(Test.foo(true))
//│ Bool
//│ res
//│     = false

This can be a convenient way of grouping definitions that share the same erased parameters.

But it is unsound to merge Test module types by treating them like the usual lattice homomorphisms:

let t = Test : Test[Int] & Test[Str]
//│ let t: Test[in Int | Str out nothing]
//│ t
//│   = Test { class: [class Test] }

t.foo
//│ (Int | Str) -> nothing
//│ res
//│     = [Function: id]

t.foo(1)("oops")
//│ nothing
//│ res
//│ Runtime error:
//│   TypeError: t.foo(...) is not a function

This is similar to how we should NOT merge (Int -> Int) & (Str -> Str) as (Int | Str) -> (Int & Str).

We should change the normal-form handling code so it is careful to avoid such unsound merges. The problem also applies to type synonyms, which should also not be merged unless we know they are lattice homomorphisms.

A related problems is that object types that need to be constructed through a constructor call can be merged in this way, but should not be valid forall-distributivity targets. For instance:

class Test[A]() {
  fun foo: A -> A = id
}
//│ class Test[A]() {
//│   fun foo: A -> A
//│ }

// Notice that the `forall` was (unsoundly) distributed, resulting in type `forall 'A. Test['A]`
fun f = Test()
//│ fun f: forall 'A. Test['A]

// Then the same unsoundness can be leveraged as before
let t = f : Test[Int] & Test[Str]
t.foo(1)("oops")
//│ let t: Test[in Int | Str out nothing]
//│ nothing
//│ t
//│   = Test {}
//│ res
//│ Runtime error:
//│   TypeError: t.foo(...) is not a function

So we should also adapt forall-distributivity to only distribute into valid target result types, such as function types or generic module types (which won't merge).