A Gradual Dependently Typed Language

Last Updated Tuesday, April 30th, 2019.

This is a thin set of macros provided on top of the redex-model for the Gradual Dependently-typed language.

Right now, this is only intended for playing around with examples from the paper. Notably, it’s very slow. Compile-time and runtime error messages are okay, but might be informative in some cases.

1 Getting Started

2 Overview of the language

3 Specific forms

First form: the dependent function type taking an argument named id of type dom to a value of type cod.

Second form: sugar for the non-dependent function type.

Third form: Sugar for (-> argtype1 (-> argtype2 ... - (> argtype_n cod) ...)).

Produces a result of type (motive discriminee).

Produces a result of type (motive length discriminee).

Produces a result of type (motive term1 term2 pf).

4 Top level commands

Any bare terms at the top-level are elaborated and evaluated. However, there are other directives we can use at the top level.

Second form: defines id to be a function of type type taking arguments x ... to result body. This is just sugar for (define id (:: (lambda (x...) body) type)).

5 Examples

Wtih s-expressions:

#lang s-exp GDTL

(define

(loop : (->

(A : (Set 10))

(B : (Set 10))

(-> (-> A B) A B )

?

A

B))

(loop A B f x = (f (lambda (y) (x x y))))

)

(define

(Z : (->

(A : (Set 10))

(B : (Set 10))

(-> (-> A B) (-> A B ))

(-> A B)))

(Z A B f = ((loop A B f) (loop A B f)))

)

We can use gradual inductive types. For example, here we use the unknown term ? as a vector length, to apply the vector head function to a vector with unknown length. At runtime, dynamic checks ensure that we throw an exception if the vector is empty.

#lang s-exp GDTL

;;We can eliminate over natural numbers to define iteration or perform induction

;;e.g. addition can be defined as follows:

(define

(plus : (-> Nat Nat Nat))

( plus m n = (NatElim m (lambda (x) Nat) n m-1 rec (Succ rec))

))

;;We can even do large elimination, to choose a type from a number

;;This lets us define the safe head function

(define

(ifzero1 : { -> Nat (Set 1) (Set 1) (Set 1) } )

(ifzero1 n S1 S2 = (NatElim 2 n (lambda (x) (Set 1)) S1 x1 x2 S2)

))

;;We eliminate a vector, producing 0:Nat if it is empty,

;; and producing its first element otherwise

;; This is type-safe because the motive of our elimination is dependent on the length of the vector

(define

(head : {-> (A : (Set 1)) (n : Nat) (Vec A (Succ n))  A })

(head A n v = (VecElim v A (Succ n) (lambda (n2 v) (ifzero1 n2 Nat A)) 0 x1 x_head x3 x4 x_head )))

;; An empty vector with  length

(define safeNil {:: (Nil Nat)  (Vec Nat 0)})

;; A non-empty vector with known length

(define safeCons {:: (Cons Nat 0 2 (Nil Nat))  (Vec Nat 1)})

;; A vector with unknown length

(define unsafeNil {:: (Nil Nat)  (Vec Nat ?)})

;; Another vector with unknown length

(define unsafeCons {:: (Cons Nat ? 2 (Nil Nat))  (Vec Nat ?)})

;;Type-checks and evaluates to 2

(head Nat 0 safeCons)

;;Does not typecheck

(head Nat ? safeNil)

;;Type-checks and evaluates to 2

(head Nat ? unsafeCons)

;;Type-checks but throws runtime exception

(head Nat ? unsafeNil)

;; We can write normal static equalities

(define 1+1=2 {:: (Refl Nat 2)

(Eq Nat 2 (plus 1 1))})

;;And a generic substitution principle

(define

(subst : (-> (A : (Set 1)) (P : (-> A  (Set 1))) (x : A) (y : A) (Eq A x y) (P x) (P y) ))

(subst A P x y pf = (EqElim

pf

A

(lambda (x1 y1 pf1) (-> (P x1) (P y1)))

z (lambda (Pz) Pz)

x

y

)))

;; And statically they fail if the two terms aren't equal

;;i.e. this does not compile

;(define 1+1=1bad {:: (Refl Nat 1)

;                  (Eq Nat 1 (plus 1 1))})

;;But we can use gradual types to type untrue equalities

(define 0=1 {:: (Refl Nat ?)

(Eq Nat 0 1)})

;;And define functions that are statically impossible

(define (magic : (-> (A : (Set 1)) (Vec A 0) (Vec A 1)))

(magic A v = (subst

Nat

(lambda (n) (Vec A n))

0

1

0=1

v

)))

;;But since our language is safe, calling these impossible functions

;; will result in a runtime error runtime error

(magic Nat (Nil Nat))

Or we can build up booleans, natural numbers, and vectors using Church encodings. This file also gives a flavour of what the language looks like with Sweet Expressions instead of S-expressions.

#lang sweet-exp GDTL

define

bool : Set(5)

bool = {(A : Set(4)) A A -> A}

define

true : bool

true A x y = x

define

false : bool

false A x y = y

define

if : {(A : Set(4)) bool A A -> A}

if A b x y =

b A x y

define

nat : Set(6)

nat = {(A : Set(5)) {A -> A} A -> A}

define

zero : nat

zero A f z = z

define

succ : {nat -> nat}

succ n A f z =

f (n A f z)

define

zero? : {nat -> bool}

zero? n =

n bool (lambda (x) false) true

define

vec : {Set(6) nat -> Set(6)}

vec A n = { (M : {nat -> Set(4)}) {(m : nat) A M(m) -> M(succ(m))} M(zero) -> M(n) }

define

head : { (A : Set(3)) (n : nat) (vec(A succ(n))) -> A}

head A n v = (v

(lambda (m)

(if Set(3) (zero? m) Set(2) A)

)

(lambda (m elem prev) elem)

Set(1)

)

define

nil : {(A : Set(6)) -> vec(A zero)}

nil A M f mz = mz

define

cons : {(A : Set(6)) (n : nat) (hd : A) (tl : vec(A n)) -> vec(A succ(n) )}

cons A n hd tl M f mz = (f n hd (tl M f mz))

define

unsafeNil : vec(Set(2) ?)

unsafeNil = { (nil Set(2)) :: vec(Set(2) ?)}

(head Set(2) zero unsafeNil)

The final line typechecks, but gives a runtime type-error.