More flexibility with types

[zeramorphic]

Type parameters should be actual parameters. For example,

def concat[T]: List[T] -> List[T] -> List[T] {
    concat Empty {} list = list
    concat Cons { value, list } other = Cons { value, list = concat list other }
}

would become something like

def concat: (T : *) -> List[T] -> List[T] -> List[T] {
    concat Empty {} list = list
    concat Cons { value, list } other = Cons { value, list = concat list other }
}

In line with this, higher kinded types would not be needed.

aspect Functor[F[_]] {
    fmap[A, B]: (A -> B) -> F[A] -> F[B]
}

might become something like

aspect Functor {
    F: * -> *
    fmap: (A: *) -> (B: *) -> (A -> B) -> F A -> F B
}

More thought should be put into the precise syntax to make it align with category theory and intuition. For instance, the above syntax for aspects would not allow consumers to constrain what type F may be; currently impl Functor[F] can be used to define the value of F.

This proposal would require reworking the type checker. De Bruijn indices would probably need to be used in types to avoid problems such as name collisions.

[zeramorphic]

Aspects and data types could be handled through the following syntax.

def Container: (T: *) -> * {
    Container T = data {
        value: T
    }
}

This would mean that the compile-time type analysis would need to be greatly improved. Syntactic sugar will likely be needed to simplify this, such as removing the def keyword which will be unnecessary.