Syntaxes for dependently typed languages

dependently_typed_syntaxes.md

Syntaxes for dependently typed languages

Luna's proposed syntax:

forall : @name arg_type return_type
lambda : #name arg_type return_body
rec    : %name recursive_term
apply  : $function argument
let    : name body

Advantages:

1. Fast (no backtracking);

2. Simple (no operators such as ->);

3. No redundancy (Idris's type/value separation names args twice);

4. Minimal noise.

Disadvantages:

1. Hard to read?

Examples

Natural number 2

Idris:

Two : Nat
Two =
  (Nat : *) ->
  (Succ : Nat -> Nat) ->
  (Zero : Nat) ->
  Succ (Succ Zero)

Morte:

Two =
  \ (Nat : *) ->
  \ (Succ : Nat -> Nat) ->
  \ (Zero : Nat) ->
  Succ (Succ Zero)

Luna:

Two
  #Nat  *        
  #Succ @ Nat Nat
  #Zero Nat      
  $Succ $Succ Zero

Simple record

Idris:

data User : Type where
  User :
    (name : String) ->
    (age : Integer) ->
    (cpf : CPF) ->
    User

Morte:

User =
  \ (Data : *) ->
  \ (User :
    \/ (name : String) ->
    \/ (age : Integer) ->
    \/ (cpf : CPF) ->
    User)
  Data

Luna:

User
  #Data *
  #User
    @name String
    @age  Integer
    @cpf  CPF
    User
  Data

Induction principle

Idris:

induction
  : (Prop : Nat -> Type) -- for any property of natural numbers
  -> (Prop Zero)         -- given a proof of `Prop(0)`
  -> (step_case :        -- given a function that
    (nat : Nat) ->       --   given a natural number `nat`
    Prop nat ->          --   given a proof of `Prop(nat)`
    Prop (Succ nat))     --   returns a proof of `Prop(Succ(nat))`
  -> (nat : Nat)         -- returns a function that, for all nat,
  -> Prop nat            -- returns a proof of `Prop(nat)`
induction Prop base_case step_case nat =
  case nat of
    Zero       => base_case
    (Succ nat) => step_case nat (induction Prop base_case step_case nat)

Morte:

induction = 
  \ (Prop : Nat -> *) ->       -- for any property of natural numbers
  \ (base_case : Prop Zero) -> -- given a proof of `Prop(0)`
  \ (step_case :               -- given a function that
    \/ (nat : Nat) ->          --   given a natural number `nat`
    (Prop nat) ->              --   given a proof of `Prop(nat)`
    Prop (Succ nat)) ->        --   returns a proof of `Prop(Succ(nat))`
  \ (nat : Nat) ->             -- returns a function that, for all nat, (returns a proof of `Prop(nat)`)
  nat base_case (step_case n (induction Prop base_case step_case n))

Luna:

induction
  #Prop @Nat *          -- for any property of natural numbers
  #base_case $Prop Zero -- given a proof of `Prop(0)`
  #step_case            -- given a function that
    @nat Nat            --   given a natural number `nat`
    @ $Prop nat         --   given a proof of `Prop(nat)`
    $Prop $Succ nat     --   returns a proof of `Prop(Succ(nat))`
  #nat Nat              -- returns a function that, for all nat, (returns a proof of `Prop(nat)`)
  $$nat base_case $$step_case n $$$$induction prop base_case step_case n