DriftLang

DriftLang is a pure functional dependently typed programming language based on GADTs. It is mostly inspired by Agda and Haskell. This programming language implements the Meadow computational model.
== Overview ==
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 & prefix.
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 and ctor2. Constructor 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.
=== Type hieararchy ===
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 Zero. Function 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 Zero and 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 Zero to 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).
== Comments ==
A comment starts with -- and extends to the end of the line.
== Syntactic sugar ==
Semicolon ; 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).
== I/O format ==
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.
Function 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 ==
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 A and 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 A and B and their constructors cA and 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 cA with A (in test1 and test2), because it is escaped, but we couldn't replace cB with B.
== Examples ==
=== Cat program ===
 main a = a
Try it online
=== Hello, World! ===
 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
Try it online
=== Reverse bits ===
 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
Try it online
=== Sort bits ===
 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
Try it online
== Interpreters ==
Interpreter
Category:Languages
Category:Turing complete
Category:2021
Category:Implemented
Category:Functional paradigm