Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
LPTK opened this issue Jan 12, 2024 · 0 comments

Comments

@LPTK
Copy link
Contributor

LPTK commented Jan 12, 2024

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

@LPTK LPTK added the soundness label Jan 12, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant