Sketch of a language

I have thought about writing a typed language for some while.

Dependent typing

A commonly accepted way to introduce dependent typing is by passing a function's variable into its type.

A function could be written like λx. value, where x is a variable and gets bound in the body. Likewise we have this extending over the type.

To illustrate how this works I better display how the call is evaluated.

(λx. value : ∏x:a. type) argument

The function type also presents the type of the argument passed in. The argument is substituted into value and type. If we represent substitution with brackets, we are going to get:

value {x:=(argument:a)} : type {x:=(argument:a)}

My problem with this approach is that it doesn't translate well for linear typing.

There's a type indexing scheme that's a variation of dependent typing. The idea is that we create types that mirror values into the type space. Then we can provide some type variables with quantifiers so we don't need to lug around the mirrored values. For example, with natural numbers we could have:

data nat¹ : nat → type where
    zero¹ : nat¹ zero
    succ¹ : nat¹ n → nat¹ (succ n)

Now we have a way to get dependent typing without duplicating values. Here's how you could ensure that predecessor is only taken from a value that has a predecessor.

predecessor : ∀x. nat¹ x → is_succ n → ∃y. nat¹ y
predecessor (succ x) refl = x

Now if we were to call this:

predecessor 3 3_is_succ

We would get to infer that 3 is nat¹ n, but there's only nat¹ like that so x = 2. And therefore we also have a simple proof for the statement.

If we abstract this out, the mirroring doesn't need to be exposed. This means that we get to represent dependent types the way they were already represented, though we have a different viewpoint to it that also relaxes the notation.

predecessor : ∀x. is_succ n → (x : nat) → nat

The type checking happens through constraint solving. Basically it could be done by augmenting bidirectional type checking with logic programming schemes.

Normal form expressions:

Expr+ → Expr+           constructs a function type
x ↦ Expr+               constructs a function
∀x. Expr+               constructs a quantifier
Var : Expr+             constructs a type mirror
case x block            constructs a case elimination
                          it's a normal form because types flow into block.
Enum [...]              constructs a tagged value.

Neutral form expressions:

Expr Expr+              function call, eliminates function
Variable                variable from the environment
EnumType [...]          enumeration type, we know what it is.

Normal-form subexpressions have been marked with +-suffix.

When a value with a quantifier is typechecked, the expression is constrained in the scope.

When type-infering provides a quantified expression, it adds a free variable into the scope.

The mirrors introduce constraints whenever they appear as types, and mirrored type may differ from the actual one, also possibly it may have to differ.

Bidirectional typechecking cues how the variables and structures in the language should behave. If we reach a variable in normal-form we can likely infer what that variable means from the context. Otherwise we have to rely on the scope.

Type declarations as structures

I think I'd like type declarations as expressions. I would likely do it this way:

maybe : type → type
maybe a = {nothing | just a}

If structures match, they're the same type.

Structured recursion

The language would not come with recursion. Instead structured recursion schemes would be used.

nat : type
nat = inductive (nat ↦ {zero | succ nat})

list : type → type
list t = inductive (list ↦ {empty | cons t list})

inductive would require that the given type is strictly positive, though it would get the proof through an implicit variable. Types could declare patterns to fill themselves up implicitly.

Abstract datatypes based on signing

Eventually you'd like something to be declared as its own type. This would be done through signing.

abstract door : {locked|unlocked|open} → type
  lock : door unlocked → door locked
  unlock : door locked → door unlocked
  open : door unlocked → door open
  close : door open → door unlocked

door = state ↦ unit
lock   nil = nil
unlock nil = nil
open   nil = nil
close  nil = nil

It would seem to fit well with the rest at the moment.

Tagless-final encoding & types

At first it'd seem like type declarations could not be deconstructed within the language once they are constructed. The problem is that 'type' cannot be a closed type. Well there's a trick around that seems to manifest in tagless-final style.

So you have some type constructor, and want to construct things out of it.

tcon : type → type

Can't deconstruct a function? Wrong! You can deconstruct this by calling the function. But can't deconstruct a type because you don't have an eliminator.

Well, how about:

tcon : type → type
sp : strictly_positive tcon

Now this is a bit different because we know what strictly positive is, and the proof describes how tcon must be structured. Given that the strict positivity is only what you need from the type, then you can use the proof to deconstruct type deep enough to provide the function you intended to provide.

Ahmad Salim Al-Sibahi in his thesis, "The Practical Guide to Levitation", attempts to provide a practical implementation of described types in Idris. If you've tried to implement decidable equality for a datatype in Idris you probably appreciate that Thesis.