# 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

### 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

### 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

### 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