Polymorphic Variants about purescript HOT 4 CLOSED

I wonder if we could get rid of the current data declarations and just have polymorphic variants. It would definitely be nice to have symmetry in the type system.

data Foo a = Foo | Bar a

would become something like

type Foo a = < Foo , Bar a >

with maybe better syntax

from purescript.

Initial attempt is in the variants branch. Code review would be appreciated.

This change removes data declarations, and now every constructor must take exactly one argument. This means that there is no exact equivalent for data Maybe a = Nothing | Just a. The nearest thing is type Maybe a = <Nothing {} | Just a>, but note that the Nothing constructor now requires an argument. This is because I can't infer the number of arguments when using the Nothing constructor on its own.

from purescript.

Moving this out of the current milestone until I can figure out what to do with nullary constructors.

One option might be to allow quantification over vectors of types, giving them their own kind V, say, so that e.g. Nothing would have type

Nothing :: forall v. v -> <Nothing :: v>

where v denotes an unknown vector of types, i.e. Nothing is a function which takes an unknown number of arguments.

Constructors would have sets of values with kind V, brought into scope in a case statement.

The case statement

case x of
  Nothing() -> ...
  Just(y) -> ...

would give the following types:

Nothing :: () -> <Nothing :: ()>
Just :: forall y. (y) -> <Just :: (y)>

This approach would probably require that unknowns cannot appear deep inside a vector. That is, a vector can either be unknown or fully known.

from purescript.

I think this has proved to be too difficult to integrate with the current sum types.

from purescript.