Total functional sublanguage typesystem

A type is either a tagged product

{on_1: type_1 , .. , on_n: type_n}

or a tagged sum

<in_1(type_1) | .. | in_n(type_n)>

Untagged product and sum types just have the default tags 'on_i' and 'in_i' filled in.
The tags are turned into functions, destructors with '.' or constructors with '&'.

let eitan: {name: string, age: int} = {name: "Eitan" , age: 33}
.name(eitan) = "Eitan"
.age(eitan) = 33

let id: <ssn(int) | email(string)> = &ssn(123456789)

We also need to be able to exhaustively match branches of sum types

let num: int = <ssn(x) -> x | email(addr) -> length(addr)>(id)

The only thing still needed to define ADTs are type aliases

type human = {name: string, age: int}
eitan: human = {name: "Eitan", age: 33}

We also want a higher kinded type alias

type list(x) = <empty_list() | cons(x,list(x))>
let mylist: list(int) = &cons(1,&cons(2,&cons(3,&empty_list())))

We can define a datatype for algebraic type syntax within Haskell as

data AlgebraicType
  = Primitive PrimitiveType
  | Product [(String,AlgebraicType)]
  | Sum [(String,AlgebraicType)]
  | TypeAlias String AlgebraicType
  | HigherTypeAlias String AlgebraicType AlgebraicType

data RhoType
  = Algebraic AlgebraicType
  | Process AlgebraicType
  | Function AlgebraicType AlgebraicType

Next, we want support a syntax sugar for various "loops".

Functor, Monad, Foldable, Traversable

A functor will mean a higher kinded type alias with a 'map' function.

type list(x) = <empty_list() | cons({head: x,tail: list(x)})>

map(f: x -> y, as: list(x)): list(y) =
  < empty_list() -> empty_list()
  | cons({head: b,tail: bs}) -> cons({head: f(b),tail: each(b <- bs) f})
  >(as)

An monad will mean a functor also with a 'yield', 'flatten' and 'flat_map' function.

yield(a: x): list(x) = &cons({head: a, tail: &empty_list()})

append(as: list(x), bs: list(x)) =
  < empty_list() -> bs
  , cons({head: c, tail: cs}) -> cons({head: c, tail: append(cs, bs)})
  >(as)

flatten(ass: list(list(x)): list(x) =
  < empty_list() -> empty_list()
  | cons({head: bs, tail: bss}) -> append(bs, join(bss))
  > ass

flat_map(f: x -> list(y), as: list(x)) = flatten(map(f, as))

A traversable will mean a functor also with a 'traverse' and 'sequence' function
...

************
Relevant papers:
https://tech.labs.oliverwyman.com/downloads/ex_nihilo_logic.pdf
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.3.9964&rep=rep1&type=ps