|Computational class||Turing complete|
There are only two things: types and functions. Function names must start with a lower-case letter. We can even use a lower-case type name by adding the
Every expression has a type. The only way to construct a type is to use some of the constructors (a constructor is a function) defined inside the type definition. For example:
MyType: ctor1 (TypeX a) = MyType a ctor2 (TypeY a) = MyType a
Here we have definition of type
MyType which has two constructors
ctor1 takes a single argument of type
TypeX and returns an instance of type
MyType with parameter
a. Similar with
ctor2. It is not possible to construct
MyType in any other way except using one of these two constructors.
It is possible to create a type hierarchy. For example, we can model natural numbers like this:
Zero: zero = Zero Succ: succ (Nat a) = Succ a Nat: nat a:Zero = Nat a nat a:(Succ *) = Nat a
We have three types. The first type
Zero has only one constructor, which takes no arguments and returns an expression of type
Succ represents the successor type. Its constructor
succ takes a natural number as argument and constructs
Succ using it. Type
Nat is a wrapper for
Succ. It can be constructed either by providing an expression of type
Zero, or an expression of type
Succ. Here, colon
: is like
@ in Haskell (as-pattern). It assigns the reference of
a. We couldn't write
Nat Zero on the right-hand-side, because we cannot use type
Zero outside of the type definition of
Zero (except in pattern-matching). The star symbol
* stands for any expression (like
_ in Haskell).
A comment starts with
-- and extends to the end of the line.
; is equivalent to a new line. Backslash
\ is equivalent to a new line followed by an implementation-dependent number of spaces (at least one space).
Input and output are arrays of bits. There are some built-in functions used for I/O actions. Basically, the following header is literally prepended before the source code before the program starts:
Bit0: bit0 = Bit0 Bit1: bit1 = Bit1 Bit: bit a:Bit0 = Bit a bit a:Bit1 = Bit a ---------------------------------------------------------------------------------------------------- Nil: nil ~t = Nil ~t Cons: cons a:(t *) (List ~t b) = Cons ~t a b List: list a:(Nil ~t) = List ~t a list a:(Cons ~t * *) = List ~t a
These six types are built-in types. The tilde symbol
~ is used to define an escaped type (like a quoted list in Lisp). In the context of
~, any type can be used, but we cannot unescape a type in pattern-matching.
main must be present in the source code. The main function is called with an expression of type
List ~Bit and the output also must be an expression of the same type.
Escaped types (the types prefixed by
~) are a bit complicated and how they behave may seem weird, but they are designed so that it is impossible to construct a real type from an escaped one outside of the constructor of the original type. The easiest way to understand
~ is to consider it as a unique built-in type. For example,
~Bit is an expression of type
~ whose value is
Bit (the value is a type).
More complex types
We can also construct more complex types, for example a list of lists of bits has type
List ~(List ~Bit).
In general, there are two ways to define an escaped version of a complex type. Suppose that we have two types
B and we want to construct escaped type
A B B B B. We can do that in two ways:
~(A B B B B) (~A B B B B)
Both ways will work, but they are not the same. The first one is preferred in most cases. These two variants are not equivalent, but it is possible to construct a function that converts one into another. Consider this example:
A: cA = A B: cB = B out2in ~(a b) = out2in ~a b out2in a = a in2out ~a = ~a in2out a = in2out (in2out_ ~a) in2out_ ~~a = ~a in2out_ ~(~a b) = ~(a b) in2out_ ~(a b) = in2out_ ~a b test1 = out2in ~(cA cB cB cB cB) test2 = in2out (~cA cB cB cB cB)
Here we have two types
B and their constructors
cB, respectively. Function
out2in converts the first variant into the second one, while
in2out converts the second variant into the first one. That is,
test1 results in
(~A B B B B), while
test2 results in
~(A B B B B).
Note: in this example, we could replace
test2), because it is escaped, but we couldn't replace
main a = a
main*=a~(~a~a~b~a~a~a~a~b~a~b~b~a~a~b~a~a~a~b~b~a~b~b~a~a~a~b~b~b~a~a~b~a~a~b~b~a~b~b~b~b~a~b~a~b~a\ ~b~b~b~a~a~b~a~a~a~a~a~a~a~b~a~b~b~a~a~a~b~b~a~b~b~b~b~a~b~b~a~b~b~a~a~a~b~b~a~b~b~a~a~a~b~b~a~a~b~\ a~b~a~b~a~a~b~a~a~a);a~~*=list(nil~Bit);a~(c d)=list(cons(bit(b d))(a~c));b~&a=bit0;b~&b=bit1
main (List ~Bit a) = list (reverse a empty) reverse &empty a = a reverse (Cons ~Bit a b) c = reverse b (cons a (list c)) empty = nil ~Bit
True: true = True False: false = False main (List * a) = list (sort a) ite True a b = a ite False a b = b sort a:&empty = a sort (Cons * a b) = join (sort (filter (gt a) b)) (cons a (list (sort (filter (lte a) b)))) filter f a:&empty = a filter f (Cons * x xs) = ite (f x) (cons x (list (filter f xs))) (filter f xs) b0 = bit bit0 b1 = bit bit1 not True = false not False = true gt &b1 &b0 = true gt * * = false lte a b = not (gt a b) join a b = reverse (reverse a empty) b reverse &empty a = a reverse (Cons * a b) c = reverse b (cons a (list c)) empty = nil ~Bit