DriftLang

DriftLang

Paradigm(s)	Functional
Designed by	User:Hakerh400
Appeared in	2021
Computational class	Turing complete
Major implementations	Interpreter
File extension(s)	.txt

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