Repository files navigation

A small functional language based on system Fω with pattern unifiction, implicit parameters, GADTs, and compilation to native.

dataNat : ∗ where| zero :Nat| succ :Nat →Natlet three= succ (succ (succ zero))dataList (a : ∗) : ∗ where| nil  :List a| (::) : a →List a →List aletnums :List Nat= zero :: succ zero :: succ (succ zero) :: three :: nil(* pattern matching*)letrec (+) (a: Nat) (b: Nat) :Nat=match awith| zero . b| succ a' . succ (a'+ b)  endletrec (++){T : ∗} (xs: List T) (ys: List T) :List T=match xswith| nil . ys| x :: xs' . x :: (xs'++ ys)  end

• function definitions
  • local definitionslet f = ... in ...
  • recursive functionslet rec
• type definitionstype t = ...
  • local type definitionslet type t = ... in ...
  • type-level lambdas
• rank N polymorphismforall x y z . t2 written as{x y z} → t2
  • optionally-explicit instantiatione {t}
• higher kinded quantification
  • kind annotations on type binders
• data declarations
  • both data parameters and indices
  • GADT syntax
  • shallow pattern matching
    • scoped type variables (without "dot patterns")
    • matching on indexed types
• user-defined infix operator
  • infix type formers
  • infix patterns
• compilation to javascript

• builtins

  • int, bool, float
  • plus, minus, times, div (for both ints and floats)
  • and, or, if
  • comparisons

• bring back∀ syntax sugar

• logging (for debugging and good errors)

• small & super simple module system and stdlib