Wipple's updated type syntax
In my spree to streamline different parts of Wipple, I've decided to update the type syntax to be more flexible and consistent. Here's how it works!
Wipple
In my spree to streamline different parts of Wipple, I’ve decided to update the type syntax to be more flexible and consistent. Here’s how it works!
The first change is that all values can be used in type position now. The type of the value is used,
sort of like an implicit typeof
operator. For example:
x : 42
f : n :: x -> n
Here, n
has type Number
. Note that this paves the way for constants as types (eg. x :: 42
)!
The second change is that data
and enum
no longer return types! Instead, they return “forms”
that expand to a value or type depending on where they are used. I already use the form pattern
throughout the Wipple compiler, so this is an easy change to make. To the user, this means that
data
and enum
effectively return “constructor” values that can be used in type position or value
position.
Integer : data ...
x : Integer 42 -- as a value
f : n :: Integer -> n -- as a type
The third change is that for
now accepts a where
clause that checks for the existence of traits:
show :: for A where (Show A) -> A -> Text
This is much better than the previous Show :: A -> _
syntax, and puts Wipple more in line with
Haskell!
In addition, pattern syntax has been extended to support datatypes and traits:
Single : data Number
Fields : data {
foo :: Number
bar :: Text
}
Trait : for A -> trait A -> A
Single n : Single 42
Fields { foo bar } : Fields {
foo : 42
bar : "hello"
}
Trait Number : n -> n
Notice that datatypes take their variables, while traits take their type parameters.
The final change is that for
may only be applied once per expression (ie. it may not be nested),
and that type parameters in traits must be filled explicitly as done above. This makes it easier to
typecheck things, and shouldn’t really even be noticeable.
Stay tuned for more updates!