MiniAgda Home Page

MiniAgda is a toy implementation of a dependently typed functional programming language. It is purpose is to try out extensions to Type Theory, such as: coinductive types, sized types for termination, extensionality for record types, erasure, subtyping.

Read

Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity
Andreas Abel, Brigitte Pientka (2013)
The 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), Boston, MA, USA, 25-27 September 2013.
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types
Andreas Abel (2012)
Invited talk at the Workshop on Fixed-points in Computer Science (FICS 2012), March 24, 2012, Tallinn, Estonia. Satellite workshop to ETAPS 2012.
.pdf .ps.gz .dvi .bib
Termination Checking: Comparing Structural Recursion and Sized Types by Examples
David Thibodeau (2011)
Student Research Report, McGill University.
MiniAgda: Integrating Sized and Dependent Types
Andreas Abel (2010)
Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010), 15 July 2010, Federated Logic Conference (FLoC 2010), Edinburgh, UK.
.pdf .ps.gz .dvi .bib
MiniAgda on the Haskell Communities and Activities Report
Termination Checking for a Dependently Typed Language
Karl Mehltretter's diploma thesis (2007)
Slides (in German).

Features and bugs

  1. Sized inductive and coinductive types.
  2. Termination check combining sized types and size-change termination a la Neil Jones.
  3. Coinductive definitional equality from Conor McBride’s Ripley cabinet. Known bug: Equality is not transitive.
  4. Erased arguments in the style of the Implicit Calculus of Constructions by Alexandre Miquel and Bruno Barras / Bruno Bernardo.
  5. Eta-expansion for Tuple types.
    2009-09-20: Extended to non-recursive constructors of non-overlapping pattern inductive families. Examples: the Identity type, the vectors of length 0.
  6. 2009-07-03: Case for inductive types (not families) which adds rewrite rules in the branches.
Report a bug!

Missing features

  1. Coverage check for pattern matching.
  2. Hidden arguments and unification.
  3. Module system.
  4. Holes and user interaction.

Download

New: From now (2014-01-09), get the latest release of MiniAgda on hackage.
    cabal install MiniAgda
    
Old instructions: MiniAgda is available as source distribution and has been tested on X86-Linux and Mac OS X. It requires a recent GHC, I am using 6.12.1, 7.0.1, and 7.4.1. Download one of the versions below, unpack, and then make or, thanks to Nils Anders Danielsson, cabal install.
Have fun!

Blog with examples

Families need not store their indices

2013-04-08: I implemented Edwin Brady's TYPES 2003 proposal that one can erase index arguments in constructors if the family indices are patterns. Concretely, I now allow a parameter to be instantiated by a pattern, similar to IDRIS-style constructors, who do not know the distinction of data parameters and data indices in the first place.

Here is what the hello world of dependent types, vectors and append function, may look like now:
data Vec ++(A : Set) (n : Nat)
{ vnil                                : Vec A zero
; vcons (vhead : A) (vtail : Vec A n) : Vec A (suc n)
} fields vhead, vtail

fun append : [A : Set] [n : Nat] [m : Nat] -> Vec A n -> Vec A m -> Vec A (plus n m)
{ append A .zero    m vnil         ys = ys
; append A (.suc n) m (vcons x xs) ys = vcons x (append A n m xs ys)
}
Since the constructor vcons no longer quantifies over n, it must be computed from the type Vec A (suc n) of the fully applied constructor. This is possible thanks to bidirectional type-checking.

On the lhs of append, we need to get hold of n somehow. Since it is absent from the constructed vcons x xs, we need to get it from the erased argument [n : Nat]. However, we cannot match on this argument with suc n, since matching on erased things is impossible (they are not there at run-time). Instead, we use the new feature of dotted constructor pattern (.suc n) which says that the only possibility here is a successor so we can project its argument n out without needing to match. Since the n is only used at an erased position on the rhs, this is fine.

We continue on the hello world! track:
data Fin (n : Nat)
{ fzero            : Fin (suc n)
; fsuc (i : Fin n) : Fin (suc n)
}

fun lookup : [A : Set] [n : Nat] (i : Fin n) (xs : Vec A n) -> A
{ lookup A .zero    ()       vnil
; lookup A (.suc n) fzero    (.vcons x xs) = x
; lookup A (.suc n) (fsuc i) (.vcons x xs) = lookup A n i xs
}
After we matched on the i : Fin n, the only case for the vector is a vcons x xs, thus, the pattern can be dotted.

A nice example are simply-typed lambda terms (see below). Note the non-linear patterns in the type of vzero : Var (cons a cxt) a.
data Ty { nat ; arr (a, b : Ty) }

let Cxt = List Ty

data Var (cxt : Cxt) (a : Ty)
{ vzero                 : Var (cons a cxt) a
; vsuc  (x : Var cxt b) : Var (cons a cxt) b
}

data Tm (cxt : Cxt) (a : Ty)

{ var (x : Var cxt a)          : Tm cxt a

; app [a : Ty] 
      (r : Tm cxt (arr a b)) 
      (s : Tm cxt a)           : Tm cxt b

; abs (t : Tm (cons a cxt) b)  : Tm cxt (arr a b)
}

Evaluation looks like this:
fun Sem : Ty -> Set
{ Sem nat       = Nat
; Sem (arr a b) = Sem a -> Sem b
}

fun Env : Cxt -> Set
{ Env nil         = Unit
; Env (cons a as) = Sem a & Env as
}

fun val : [cxt : Cxt] [a : Ty] -> Var cxt a -> Env cxt -> Sem a
{ val (.cons a cxt) .a vzero   (v, vs) = v
; val (.cons a cxt) b (vsuc x) (v, vs) = val cxt b x vs
}

fun sem : [cxt : Cxt] [a : Ty] -> Tm cxt a -> Env cxt -> Sem a
{ sem cxt a          (var x)     rho   = val cxt a x rho
; sem cxt b          (app a r s) rho   = (sem cxt (arr a b) r rho) (sem cxt a s rho)
; sem cxt (.arr a b) (abs t)     rho v = sem (cons a cxt) b t (v, rho)
}

Instantiation to infinity

2013-04-05: A bounded existential quantifier [i < #] & F i can now be instantiated to # if F is lower semi-continuous, for instance, if it is antitone or an inductive type of size i.
data Maybe ++(A : Set) { nothing ; just (a : A) }

cofun Nat : +Size -> Set
{ Nat i = [j < i] & Maybe (Nat j)
}

pattern pzero i   = i , nothing
pattern psucc i n = i , just n

let zeroInf             : Nat # = pzero #
let succInf (n : Nat #) : Nat # = psucc # n
Analogously, a bounded universal quantifier [i < #] -> F i can now be instantiated to # if F is upper semi-continuous, for instance, if it is monotone or a coinductive type of size i.
record Prod ++(A, B : Set) { pair (fst : A) (snd : B) } fields fst, snd

cofun Stream : ++(A : Set) -> -(i : Size) -> Set
{ Stream A i = [j < i] -> Prod A (Stream A j)
}

pattern cons x xs = pair x xs

let head [A : Set] (s : Stream A #) : A           =  s # .fst
let tail [A : Set] (s : Stream A #) : Stream A #  =  s # .snd 

A paradox connected to careless handling of infinite size

2013-04-02: We can encode all of untyped lambda calculus exploiting MiniAgda' careless handling of infinity.
cofun D : Size -> Set
{ D i = [j < i] -> |i| < |$$j| -> D j -> D j
}
The constraints effectively express that i = $j. However, they also exclude i = #. We will exploit the fact that MiniAgda does not require i < # to infer i < $i to work around the constraints and instantiate i to # nevertheless.
fun app_ : [i : Size] -> D $i -> D i -> D i
{ app_ i f = f i
}
Here, f of type

  [j < $i] -> |$i| < |$$j| -> D j -> D j
is instantiated with i < $i, which is invalid with for i = # under # = $#, to
  |$i| < |$$i| -> D i -> D i
which is just D i -> D i. Thus app_ should only have type [i < #] -> D $i -> D i -> D i. In this case, we could not make the following instantiation i = #.
let app : D # -> D # -> D # = app_ #
Now, towards abstraction...
fun abs_ : [i : Size] -> (D i -> D i) -> D $i
{ abs_ i f j = f
}
This type-checks because the constraints j < $i and $i < $$j guarantee i = j. However, MiniAgda should not accept the constraints on j unless i < #. The rest is easy:
let abs : (D # -> D #) -> D # = abs_ #
let delta : D # = abs (\ x -> app x x)
let Omega : D # = app delta delta
There are two ways out: The first, already implemented but deactivated, distinguishes size variables strictly below infinity from those that can also be instantiated with infinity. However, I am tending more towards giving up on $# = #, this might be clearer to the user. Of course, we need to identify situations in which we can still treat # + n as #.

2013-04-05: A third alternative is to forbid type D because it is discontinuous. Precisely, D # is distinct from D i for all ordinals i < #. Such types should probably be rejected by MiniAgda.

Harmful bounded lambda abstractions

2013-03-30: Here is a use of a bounded lambda-abstraction that destroys strong normalization.
data Unit { unit }

fun sabotage : [i : Size] -> ([j < i] -> Unit) -> Unit
{ sabotage i f = unit
}

fun notSN : [i : Size] -> |i| -> Unit
{ notSN i = sabotage i (\ j -> notSN j)
}
Apparently, notSN is not strongly normalizing. The lambda on the r.h.s. introduces a size variable j < i, however, it is not guaranteed that this is always possible, e.g., when i = 0. Such lambdas are henceforth forbidden, unless you use cofun which does not aim at strong normalization.

Mixed inductive-coinductive types

2012-01-28: Before diving into today's topic, let us give an example how to define a data type instead of declaring it.
-- * Booleans

data Bool { true ; false } 

fun If : Bool -> ++(A, B : Set) -> Set
{ If true  A B = A
; If false A B = B
}

-- * disjoint sum

let Either ++(A, B : Set) = (b : Bool) & If b A B

pattern left  a = (true  , a)
pattern right b = (false , b)
Like in PiSigma, we can bootstrap data types from function type (->), pair type (&), labels or tags (like true and false), and definition by cases (If) and recursion (see below). pattern declarations are a convenience to make code easier to read and write, they are nothing but macros, yet only consisting of constructors. The type of streams is defined by recursion:
cofun Stream : ++(A : Set) -> -(i : Size) -> Set
{ Stream A i = [j < i] -> A & (Stream A j)
}

pattern cons x xs = x , xs
The definition says that when you apply a stream s : Stream A i to a size j which is below i, then you get a pair consisting of the head of type A and the tail of type Stream A j. The guardedness level j of the tail is strictly below the guardedness level i of the whole stream.

An s : Stream A # is a stream which can be unrolled infinitely often (# being concrete syntax for ∞), this is the beast we are interested in. We can always take the head of such a stream:
let head [A : Set] (s : Stream A #) : A
  = case (s 0) { (cons x xs) -> x }
Note that by applying s to 0 we get an unguarded stream xs : Stream A 0, but we do not care, since it is thrown away.

We can always take the tail of an ∞-stream as well. However, this needs a little justification. Basically, we need to convince the type checker that Stream A # is the greatest fixed-point of F X = A & X. Such a fixed-point exists because the operator F is strictly-positive. However, MiniAgda never checked this, since the definition of Stream was by recursion, and the only requirement for recursive definition is termination. (Termination holds since the recursive call Stream A j has decreased the second argument compared to the l.h.s. Stream A i.)

To define the tail operation, we use the fact that j < ∞ implies j+1 < ∞.
fun tail : [A : Set] -> Stream A # -> Stream A #
{ tail A s (j < #) = case (s $j) { (cons x xs) -> xs j }
} 
Unrolling the stream tail A s : Stream A # at guardedness level j is performed by first unrolling stream s at guardedness level j+1. This yields a pair cons x xs whose second component xs : Stream A $j can be unrolled at level j to produce the desired result, the unrolled tail.

Now to our topic, mixed inductive-coinductive data types. Stream processors SP A B are a representation of continuous functions from streams over A to streams over B. Here is a Haskell representation:
data SP a b = Get (a -> SP a b) | Put b (SP a b)

run :: SP a b -> [a] -> [b]
run (Get f)    as = run (f (head as)) (tail as)
run (Put b sp) as = b : run sp as 
Function run, called eat in the linked publication, executes a stream processor, i.e., turns it into an actual function from streams to streams.

In general, run sp might not be productive, i.e., consume stream as forever without outputting a single b. To prevent this, we require that stream processors only have finitely many Gets between two Puts. This can be achieved by nesting an inner, inductive, fixed-point which handles the gets into an outer, coinductive fixed-point which accunts for the puts..

In MiniAgda, we can define a mixed coinductive-inductive type by using both bounded existential (induction) and bounded universal quantification (coinduction).
cofun SP : -(A : Set) -> ++(B : Set) -> -(i : Size) -> +(j : Size) -> Set
{ SP A B i j = Either ([j' < j] & (A -> SP A B i j'))   -- get
                      (B & ([i' < i] -> SP A B i' #))   -- put
}
pattern get j f  = left  (j , f) 
pattern put b sp = right (b , sp)
The first constructor, get, is inductive, while the second, put, is coinductive. The two size indices i and j form a lexicographic product, where the index i for coinduction is the primary and the index j for induction the secondary component. The termination checker infers this order from the recursive calls, but we can also explicitly specify it:
cofun SP : -(A : Set) -> ++(B : Set) -> -(i : Size) -> +(j : Size) -> |i,j| -> Set
The run function terminates by the same order. This time, we have to specify it explicitly.
cofun run : [A, B : Set] -> [i, j : Size] -> |i,j| -> SP A B i j -> Stream A # -> Stream B i
{ run A B i j (get j' f) as          = run A B i j' (f (head A as)) (tail A as)
; run A B i j (put b sp) as (i' < i) = cons b (run A B i' # (sp i') as) 
}
MiniAgda answers that it understood the following:
term  run : .[A : Set] -> .[B : Set] -> .[i : Size] -> .[j : Size] -> SP A B i j -> Stream A # -> Stream B i
{ run [A] [B] [i] [j] (true, ([j'], f)) as = run [A] [B] [i] [j'] (f (head [A] as)) (tail [A] as)
; run [A] [B] [i] [j] (false, (b, sp)) as [i' < i] = (b , run [A] [B] [i'] [#] (sp [i']) as)
}
If you drop everything enclosed in [brackets], you get the Haskell program (modulo encoded constructors)! Great, isn't it?
term  run : SP A B i j -> Stream A # -> Stream B i
{ run (true, f)        as = run (f (head as)) (tail as)
; run (false, (b, sp)) as = (b , run sp as)
}

New telescope syntax for let

2012-01-27: Telescopes are now allowed in let definitions. Also, the type of a let can be left out if it is inferable (in the sense of bidirectional checking). Examples:
-- Telescopes in let-declarations
----------------------------------------------------------------------

-- instead of

let two : [A : Set] -> (f : A -> A) -> (a : A) -> A
  = \ A f a -> f (f a)

-- one can now write

let two1 [A : Set] (f : A -> A) (a : A) : A
  = f (f a)

-- since the type A of the let-body f (f a) is inferable
-- we can omit it

let two2 [A : Set] (f : A -> A) (a : A)
  = f (f a)

-- Untyped local let
----------------------------------------------------------------------

-- inferable types of local let declarations can also be omitted

let twice [F : Set -> Set] (f : [A : Set] -> A -> F A)
          [A : Set] (a : A) : F (F A)
  = let [FA] = F A   in
    let fa   = f A a in f FA fa

-- local lets can also use telescopes
let localLetTel : Size =
  let two1 [A : Set] (f : A -> A) (a : A)
    = f (f a)
  in 0

-- and can still be made irrelevant
let localLetIrr [A : Set] (f : [A -> A] -> Size) [a : A] : Size =
  let [g] (x : A) = a
  in  f g

-- alternative with . instead of brackets
let localLetIrr1 [A : Set] (f : .(A -> A) -> Size) .(a : A) : Size =
  let .g (x : A) = a
  in  f g

New constructor syntax II

2012-01-27: Telescopes are now allowed in constructor declarations, and the target can be omitted if it is not a family (GADT). Thus, the Maybe type can be declared as:
data Maybe (A : Set) 
{ nothing 
; just (a : A)
}

New constructor syntax

2012-01-23: I decided to remove parameter arguments from constructors, as it is in Agda. Now, there is a bit fewer boilerplate to type. New syntax:
-- data declarations as before
data Maybe (A : Set) 
{ nothing : Maybe A
; just    : A -> Maybe A
}

-- parameter A no longer needed in constructor patterns and terms
fun mapMaybe : [A, B : Set] -> (A -> B) -> Maybe A -> Maybe B
{ mapMaybe A B f nothing = nothing
; mapMaybe A B f (just a) = just (f a)
}

Greatest common divisor (example)

2011-12-16: Here is a useful example with bounded quantification in an auxiliary function:
sized data Nat : Size -> Set 
{ zero : [i : Size] -> Nat ($ i)
; suc  : [i : Size] -> Nat i -> Nat ($ i)
}

-- subtracting two numbers with minus yields the difference
-- plus a bit indicating the bigger number of the two

data Either : +Size -> +Size -> Set
{ left  : [i,j : Size] -> Nat i -> Either i j
; right : [i,j : Size] -> Nat j -> Either i j
}

fun minus : [i,j : Size] -> Nat i -> Nat j -> Either i j
{ minus i j (zero (i > i'))   m                 = right i j m 
; minus i j (suc  (i > i') n) (zero (j > j'))   = left i j (suc i' n)
; minus i j (suc  (i > i') n) (suc  (j > j') m) = minus i' j' n m
}

-- greated common divisor (gcd) in "Agda-with" style
-- uses an auxiliary function distinguishing over the result of subtraction
-- note how bounded quantification is used to maintain size relations

mutual {

  fun gcd : [i,j : Size] -> Nat i -> Nat j -> Nat #
  { gcd i j (zero (i > i')) m = m
  ; gcd i j (suc (i > i') n) (zero (j > j')) = suc i' n
  ; gcd i j (suc (i > i') n) (suc (j > j') m) = 
      gcd_aux i j i' j' n m (minus i' j' n m)
  }

  fun gcd_aux : [i,j : Size] -> [i' < i] -> [j' < j] -> Nat i' -> Nat j' ->
                Either i' j' -> Nat #
  { gcd_aux i j i' j' n m (left  .i' .j' n') = gcd i' j n' (suc j' m)
  ; gcd_aux i j i' j' n m (right .i' .j' m') = gcd i j' (suc i' n) m'
  }
} 

Bounded size quantification

2010-11-12: Bounded size quantification is now experimentally supported. Intended use is [j : Size] -> |j| <= |i| -> or [j : Size] -> |j| < |i| -> for i a size variable. If you tread beyond these pathes, weird and buggy stuff might happen.

Here some useless examples:
sized data Nat : Size -> Set
{ zero : [i : Size] -> Nat $i
; succ : [i : Size] -> Nat i -> Nat $i
}

let mySucc : [i : Size] -> [j : Size] -> |j| < |i| -> Nat j -> Nat i
 = \ i j n -> succ j n 

let boundedId : [i : Size] -> [j : Size] -> |j| <= |i| -> Nat j -> Nat j
  = \ i j n -> n

fun explicitCast : [i : Size] -> [j : Size] -> |j| <= |i| -> Nat j -> Nat i
{ explicitCast i j n = n
}

3 Function spaces: irrelevant, parametric, recursive

2010-11-09: Working towards a representation of parametric functions in MiniAgda. This is sometimes called the LF function space. I'd call it parametric function space. It contains the functions that do not analyze their argument but may store it in some structure. (In contrast, irrelevant functions discard their argument.) Functions that do analyze their argument I call recursive. The prototypical parametric functions are the pure (typed) lambda-calculus and data constructors. Anything that involves (non irrefutable) pattern-matching is computational (recursive) and not parametric.

The characterization of function spaces is done via polarities. In general, function space is written p(x : A) -> B. The following polarities are available.
  .     Constant/irrelevant function
  ++    Strictly positive   function (types only)
  +     Monotone            function (types only)
  -     Antitone            function (types only)
  ^     Parametric (lambda) function
  *     Recursive           function
If no polarity is given, MiniAgda tries to put some reasonable default (work in progress). Constructor types are parametric by default (the only other sensible polarity here is "e;irrelevant"e;). Data type telescopes are parametric in the data type and irrelevant in the constructor types. Sometimes a data type parameter needs to be declared as recursive, e.g.
data AccPar (A : Set) (Lt : A -> A -> Set) *(b : A) : Set
{ accPar :  (accParOut : (a : A) -> Lt a b -> AccPar A Lt a) -> AccPar A Lt b
} 
Since Lt : *A -> *A -> Set (default is recursive!) is a predicate which may analyse its arguments, AccPar needs to be declared recursive in b, otherwise the call Lt a b would be rejected.

Here, an example where all polarities are given explicitly.
let Const : ++Set -> .Set -> Set 
          = \ A -> \ X -> A

let DNeg : ^ Set -> +Set -> Set
         = \ B -> \ A -> * (* A -> B) -> B

data Empty : Set {}

data Cont +(A : Set) : Set 
{ cont : (uncont : DNeg Empty A) -> Cont A
}

sized data Nat : + Size -> Set
{ zero : [i : Size] -> Nat ($ i)
; succ : [i : Size] -> Nat i -> Nat ($ i)
}

let cast : [i : Size] -> ^ Cont (Nat i) -> Cont (Nat #)
         = \ i -> \ x -> x

fun Id : * Nat # -> ++Set -> Set
{ Id (zero .#)   A = A
; Id (succ .# n) A = A
}

let kast : [i : Size] -> [n : Nat i] -> ^ Id n (Nat i) -> Id n (Nat #)
         = \ i -> \ n -> \ x -> x
Now, [x : A] -> B is identified with .(x : A) -> B. MiniAgda currently prints it as .[x : A] -> B.

Size addition

2010-11-01: Size addition has been added to MiniAgda, but is not systematically supported yet. Especially size constraint solving is more difficult with addition, becoming a MAXPLUS constraint problem. A few simple examples work already, for instance the evens function suggested to me by Florent Balestrini:
sized codata Stream ++(A : Set) : -Size -> Set 
{ cons : [i : Size] -> (head : A) -> (tail : Stream A i) -> Stream A $i
}

cofun evens : [A : Set] -> [i : Size] -> Stream A (i + i) -> Stream A i
{ evens A ($i) (cons .A .(i + i + 1) a (cons .A .(i + i) b as)) =
   cons A i a (evens A i as)
}

cofun map2 : [A, B : Set] -> (A -> B) -> 
             [i : Size] -> Stream A (i + i) -> Stream B (i + i)
{ map2 A B f ($ i) (cons .A .$(i + i) a1 (cons .A .(i + i) a2 as)) =
    cons B $(i + i) (f a1) (cons B (i + i) (f a2) (map2 A B f i as))
}

Heterogeneous Algorithmic Equality

2010-10-01: When you combine dependent irrelevant quantification with large eliminations, the equality test needs to be heterogeneous in some cases, e.g., the compared expressions need to come with their own type in their own context. The following example was presented to me by Ulf Norell during AIM 11:
fun T : Bool -> Set
{ T true  = Nat
; T false = Bool
}

fun bad : 
  [F : Nat -> Set] ->
  [f : [x : Bool] -> T x -> Nat] ->
  (g : (n : Nat) -> F (f true n)) ->
  (h : F (f false false) -> Bool) -> 
  Bool
{ bad F f g h = h (g zero)
}
h expects an argument of type F (f false false) but gets one of type F (f true zero). Comparing the spines of f we skip the first argument of type Bool, since it is declared irrelevant. The second argument is now false : Bool on the one hand and zero : Nat on the other hand. Thus, we come to compare expressions at different types. MiniAgda thus has a heterogeneous algorithmic equality, which fails as soon as it has to compare expressions at types of a different shape. For instance, comparing a function to a number will fail because the types cannot be reconciled. In the above example, Bool and Nat are two differend data types which are not compatible.

This is not terribly inefficient: To check shapes for compatibility, the weak head normal form of the involved types is sufficient.

Proof Monad

2010-09-22: Today's improvement of deep matching in irrelevant context let's me type check the multiplication (join) of the proof monad (also called Squash) without trustme.
data Prf ++(A : Set) : Set
{ prf : [A] -> Prf A
}

fun elimPrf : [A : Set] -> [P : Prf A -> Set] ->
              (f : [a : A] -> P (prf A a)) ->
              [x : Prf A] -> P x
{ elimPrf A P f (prf .A a) = f a 
}

-- monad operations for Prf

fun mapPrf : [A, B : Set] -> (A -> B) -> Prf A -> Prf B
{ mapPrf A B f (prf .A a) = prf B (f a)
}

fun joinPrf : [A : Set] -> Prf (Prf A) -> Prf A
{ joinPrf A (prf .(Prf A) (prf .A a)) = prf A a
}

let bindPrf : [A, B : Set] -> Prf A -> (A -> Prf B) -> Prf B
  = \ A B pa f -> joinPrf B (mapPrf A (Prf B) f pa)

Expression classification

2010-09-20: MiniAgda now classifies expressions into terms, type (constructors)s, and universe(constructor)s. This is an important step towards program extraction, but it also improves the analysis which arguments of a function can contribute to the computation of the result. A simple example:
f : (A : Set) -> (x : A) -> A
No matter how f is defined, the type argument A cannot contribute to the result, since types cannot be matched on (no typecase!), and A cannot be returned as part of the result since A is not an element of A.
B : Set
g : (A : Set) -> (A -> B) -> B
Here, the first argument of g is again irrelevant, since result type B can hold terms, not types like A. MiniAgda also marks index arguments in constructors irrelevant, as described in Edwin Brady's thesis (and his TYPES 2003 paper).
data Vec (A : Set) : Nat -> Set
{ nil  : Vec A zero
; cons : (n : Nat) -> A -> Vec A n -> Vec A (succ n)
}

{- MiniAgda output
type  Vec  : (A : Set) -> Nat -> Set
term  nil  : [A : Set] -> Vec A zero
term  cons : [A : Set] -> [n : Nat] -> A -> Vec A n -> Vec A (succ n)
-}
MiniAgda classifies Vec as type (this is not hard, it lives in Set). Constructors are always classified as terms. Not only the parameter A : Set is marked as irrelevant in the constructors, but also the index n : Nat in cons. This is soundsince if you want to know the length of a vector, the type system requires you to already have it, so you do not need to look inside of cons.
fun length : (A : Set) -> (n : Nat) -> Vec A n -> Nat
{ length A n v = n
}

{- MiniAgda output
term  length : [A : Set] -> (n : Nat) -> Vec A n -> Nat
{ length [A] n v = n
}
-}
MiniAgda's erasure could be more aggressive here, also dump the vector v : Vec A n. Future work...

In the destructors, you can see erasure in action.
fun head : (A : Set) -> (n : Nat) -> Vec A (succ n) -> A 
{ head .A .m (cons A m x xl) = x
}

{- MiniAgda output
term  head : [A : Set] -> (n : Nat) -> Vec A (succ n) -> A
{ head [.?0] .?1 (cons [A] [m] x xl) = x
}
-}
Currently, you have to be careful where you place the dots in the patterns.
fun append : (A : Set) -> (n, m : Nat) -> Vec A n -> Vec A m -> Vec A (add n m)
{ append .A .zero     m (nil A)         v = v
; append .A .(succ n) m (cons A n x xl) v = cons A (add n m) x (append A n m xl v)
}

{- MiniAgda output

term  append : [A : Set] -> (n : Nat) -> (m : Nat) -> Vec A n -> Vec A m -> Vec A (_add n m)

error during typechecking:
append
/// clause 2
/// right hand side
... variable n : Nat may not occur
/// , because it is marked as erased
-}
Since MiniAgda is not smart enough that n, m : Nat are irrelevant, it complains that we extracted n from an irrelevant argument of cons and try to use it on the r.h.s. in a computational meaningful way (so it thinks). The following dotting works.
fun append : (A : Set) -> (n, m : Nat) -> Vec A n -> Vec A m -> Vec A (add n m)
{ append A .zero    m (nil  .A)         v = v
; append A (succ n) m (cons .A .n x xl) v = cons A (add n m) x (append A n m xl v)
}

{- MiniAgda output
term  append : [A : Set] -> (n : Nat) -> (m : Nat) -> Vec A n -> Vec A m -> Vec A (_add n m)
{ append [A] .?1 m (nil [.?3]) v = v
; append [A] (succ n) m (cons [.?3] [.?4] x xl) v = cons [A] [_add n m] x (append [A] n m xl v)
}
-}
Classification and irrelevance inference does not yet work for universe-polymorphic things.

Mutual data types

2010-08-28: MiniAgda now supports mutual data types.
mutual {

  data Even : Set 
  { ev0 : Even
  ; evS : Odd -> Even
  }

  data Odd : Set
  { oddS : Even -> Odd
  }

}

data Nat : Set
{ zero : Nat
; suc  : Nat -> Nat
}

mutual {

  fun evenToNat : Even -> Nat
  { evenToNat ev0 = zero
  ; evenToNat (evS o) = suc (oddToNat o)
  }

  fun oddToNat : Odd -> Nat
  { oddToNat (oddS e) = suc (evenToNat e)
  }
} 

Measures

2010-07-27: Following ideas of Hongwei Xi (LiCS 2001), one can now explicitely state the termination argument using measures |s1,...,sn| which are compared lexicographically.
data Bool : Set
{ true : Bool
; false : Bool
}

sized data Nat : Size -> Set
{ zero : [i : Size] -> Nat ($ i)
; succ : [i : Size] -> Nat i -> Nat ($ i)
}

mutual {

  fun even  : [i : Size] -> |i,$0| -> Nat i -> Bool
  { even i n = even' i n
  }

  fun even' : [i : Size] -> |i,0|  -> Nat i -> Bool
  { even' i (zero (i > j))   = true
  ; even' i (succ (i > j) n) = odd' j n
  } 

  fun odd'  : [i : Size] -> |i,0|  -> Nat i -> Bool
  { odd' i (zero (i > j))   = false
  ; odd' i (succ (i > j) n) = even j n
  } 
}
Sometimes we need bounds to explain termination. Below we use bounded size quantification [j : Size] -> |j| < |i| -> Stack A j -> A -> Stack A j in function pushFunc to show that pushFix is productive. Note that the recursive call pushFix A on the right hand side has the abovementioned bounded type.
data Maybe (A : Set) : Set
{ nothing : Maybe A
; just : A -> Maybe A
}

-- stack object
sized codata Stack (A : Set) : Size -> Set
{ stack : [i : Size] ->
  (top  : Maybe A) ->
  (pop  : Stack A i) ->
  (push : A -> Stack A i) -> Stack A $i
} 

-- functional to construct push action
cofun pushFunc : [A : Set] -> [i : Size] -> |i| ->
                 ([j : Size] -> |j| < |i| -> Stack A j -> A -> Stack A j) ->
                 Stack A i -> A -> Stack A i
{ pushFunc A ($ i) f s a = stack A i (just A a) s (f i (pushFunc A i f s a))
} 

-- tying the knot
cofun pushFix  : [A : Set] -> [i : Size] -> |i| -> Stack A i -> A -> Stack A i
{ pushFix A ($ i) = pushFunc A ($ i) (pushFix A)
}

-- constructing the empty stack
cofun empty : [A : Set] -> [i : Size] -> |i| -> Stack A i
{ empty A ($ i) = stack A i (nothing A) (empty A i) (pushFix A i (empty A i))
}

Universe polymorphism

Set : Set has been replaced by a predicative hierarchy Set 0 <= Set 1 <= ...
data List [i : Size](A : Set i) : Set i
{ nil  : List i A
; cons : A -> List i A -> List i A
}
 

Polarity annotations

2010-06-20: Polarities are now first-class. Functions can carry a polarity in front of their domain to characterize their monotonicity behavior.

This is how they are used:

 pmeaning of polarity
 ++strictly positive
 +positive (covariant,monotone)
 -negative (contravariant,antitone)
 /constant (invariant)
 (none)arbitrary (mixed variant)
-- A-labelled B-branching Trees

data Tree -(B : Set) ++(A : Set) : Set
{ leaf : Tree B A
; node : A -> (B -> Tree B A) -> Tree B A
}

-- sized inductive types

sized data Mu ++(F : ++Set -> Set) : +Size -> Set
{ inn : [i : Size] -> (out : F (Mu F i)) -> Mu F ($ i)
}

-- iteration (universal property of initial F-algebra Mu)
fun iter : [F : ++Set -> Set] -> 
           (mapF : [A : Set] -> [B : Set] -> (A -> B) -> F A -> F B) ->
           [G : Set] -> (step : F G -> G) ->
           [i : Size] -> Mu F i -> G
{ iter F mapF G step i (inn .F (i > j) t) =
   step (mapF (Mu F j) G (iter F mapF G step j) t)
}

-- natural numbers

data Unit : Set 
{ unit : Unit 
}
data Sum ++(A : Set) ++(B : Set) : Set
{ inl : A -> Sum A B
; inr : B -> Sum A B
}

let NatF : ++Set -> Set = \ X -> Sum Unit X
let Nat  : +Size -> Set = Mu NatF

let zero : [i : Size] -> Nat ($ i)
         = \ i -> inn NatF i (inl Unit (Nat i) unit) 

let succ : [i : Size] -> Nat i -> Nat ($ i)
         = \ i -> \ n -> inn NatF i (inr Unit (Nat i) n) 

Corecursive Functions Returning a Tuple

2010-06-08: Jones and Gibbons (1993) present a circular program that relables a possibly infinite binary tree in breath-first order, taking labels from an infinite stream. Conor McBride showed me this example on a flight back from Tallinn in 2007 (if I remember correctly), and we conjectured that it can be handled with sized types. Nils Anders Danielsson treats it in his paper Beating the Productivity Checker presented at the workshop on Partiality and Recursion in Interactive Theorem Provers (PAR'10). Now I have modified MiniAgda to accept this example.

Let us first define the types of Cartesian product, streams and possibly infinite trees. Prod is a record with two fields fst and snd.
data Prod (+ A : Set)(+ B : Set) : Set 
{ pair : (fst : A) -> (snd : B) -> Prod A B
}

sized codata Stream (+ A : Set) : Size -> Set
{ cons : [i : Size] -> (head : A) -> (tail : Stream A i) -> Stream A ($ i)
}

sized codata Tree (+ A : Set) : Size -> Set 
{ leaf : [i : Size] -> Tree A ($ i)
; node : [i : Size] -> A -> Tree A i -> Tree A i -> Tree A ($ i)
}
The heart of the example is the corecursive function lab which returns a pair of the relabled tree and the remaining stream-stream of labels. If we split it in two functions, one returning the relabelled tree, and one returning the remaining labels, we have two "e;proper"e; corecursive function, returning something of coinductive type, but then all efficiency is lost. However, as verified in my TLCA 2003 paper, a corecursive function can also return a cartesian product of coinductive types. It is crucial that both types are indexed by the same size variable i.
cofun lab : [i : Size] -> [A : Set] -> [B : Set] ->
   Tree A i -> Stream (Stream B #) i -> 
   Prod (Tree B i) (Stream (Stream B #) i)
{
  lab ($ i) A B (leaf .A .i) bss = 
    pair (Tree B ($ i)) (Stream (Stream B #) ($ i)) (leaf B i) bss

; lab ($ i) A B (node .A .i x l r) 
    (cons .(Stream B #) .i (cons .B .# b bs) bss) =

      -- recursive call on left subtree
      let    pl   : Prod (Tree B i) (Stream (Stream B #) i)
                  = lab i A B l bss 

      -- recursive call on right subtree, threading the label stream-stream
      in let pr   : Prod (Tree B i) (Stream (Stream B #) i)
                  = lab i A B r (snd (Tree B i) (Stream (Stream B #) i) pl) 

      in pair (Tree B ($ i)) (Stream (Stream B #) ($ i))
           (node B i b (fst (Tree B i) (Stream (Stream B #) i) pl)
                       (fst (Tree B i) (Stream (Stream B #) i) pr))
           (cons (Stream B #) i bs 
                       (snd (Tree B i) (Stream (Stream B #) i) pr))
}
Following Danielsson, we represent the cycle in the original program by a corecursive function label2. The main function label calls lab with an initial stream-stream generated by label2.
cofun label2 : [i : Size] -> [A : Set] -> [B : Set] -> 
  Tree A i -> Stream B # -> Stream (Stream B #) i 
{ label2 ($ i) A B t bs = snd (Tree B ($ i)) (Stream (Stream B #) ($ i))
    (lab ($ i) A B t (cons (Stream B #) i bs (label2 i A B t bs)))
}

fun label : [i : Size] -> [A : Set] -> [B : Set] -> 
  Tree A i -> Stream B # -> Tree B i
{ label i A B t bs = fst (Tree B i) (Stream (Stream B #) i)
   (lab i A B t (cons (Stream B #) i bs (label2 i A B t bs)))
}
Here is some code to test the program.
data Unit : Set
{ unit : Unit
}

data Nat : Set 
{ Z : Nat
; S : Nat -> Nat
}

cofun nats : [i : Size] -> Nat -> Stream Nat i
{ nats ($ i) n = cons Nat i n (nats i (S n))
}

fun finTree : Nat -> Tree Unit #
{ finTree Z = leaf Unit #
; finTree (S n) = node Unit # unit (finTree n) (finTree n)
}

eval let t0 : Tree Nat # = label # Unit Nat (finTree Z) (nats # Z)
eval let t1 : Tree Nat # = label # Unit Nat (finTree (S Z)) (nats # Z)
eval let t2 : Tree Nat # = label # Unit Nat (finTree (S (S Z))) (nats # Z)
eval let t3 : Tree Nat # = label # Unit Nat (finTree (S (S (S Z)))) (nats # Z)
It was necessary to change the evaluation strategy of MiniAgda from call-by-value to call-by-name, since eager constructors destroy strong normalization even if cofuns are only unfolded by demand. To see this, consider the same program in Haskell (to save ourselves from tiring type arguments).
data P a b    = P !a !b; 
data Stream a = C !a (Stream a);
data Tree a   = L 
              | N !a (Tree a) (Tree a);
fst (P a b) = a;
snd (P a b) = b;

--lazy lab
lab :: Tree a -> Stream (Stream b) -> P (Tree b) (Stream (Stream b))
lab  L         bss             = P L bss;
lab (N x l r) (C (C b bs) bss) =
  let    pl = lab l bss
  in let pr = lab r (snd pl)
  in P (N b (fst pl) (fst pr))
       (C bs (snd pr));

--lazy label2
label2 :: Tree a -> Stream b -> Stream (Stream b)
label2 t bs = snd (lab t (C bs (label2 t bs)));

label :: Tree a -> Stream b -> Tree b
label t bs = fst (lab t (C bs (label2 t bs)));
The cofuns lab and label2 are only unfolded if their result is analyzed by pattern matching. Let t = N x t t an infinite tree and bs = C y bs and infinite stream and consider computing the weak head normal form of label t bs. It unfolds to a fst (lab ...) which forces unfolding of cofun lab. This, in case the constructors N and C are strict, again computes fst (lab ...) which again forces lab. This continues forever, never returning the weak head normal form.

Thus, I need to depart from the strategy of my thesis which only required lazy cofun unfolding. Now constructors must also be lazy, hence, we need to depart from call-by-value.

Large Eliminations and Sized Types

2010-05-08: MiniAgda allows the following sized typing of the binary maximum function on natural numbers.
sized data Nat : Size -> Set
{ zero : [i : Size] -> Nat ($ i)
; succ : [i : Size] -> Nat i -> Nat ($ i)
}

fun max2 : [i : Size] -> Nat i -> Nat i -> Nat i
{ max2 i (zero (i > j))    n               = n
; max2 i  m               (zero (i > j))   = m
; max2 i (succ (i > j) m) (succ (i > k) n) = 
   let [h : Size] = max j k 
   in  succ h (max2 h m n)
}
In this example, we introduce a new irrelevant variable h through a let binding.

An n-ary maximum can also be defined via a recursively defined sized type Maxs.
fun Maxs : Nat # -> Size -> Set
{ Maxs (zero .#  ) i = Nat i
; Maxs (succ .# n) i = Nat i -> Maxs n i
}

fun maxs : (n : Nat #) -> [i : Size] -> Nat i -> Maxs n i
{ maxs (zero .#)   i m = m
; maxs (succ .# n) i m = \ l -> maxs n i (max2 i m l)
}

Coinductive types II

2010-03-12: Getting coinduction right!

The following looks ok, but is flawed. (Thanks to Nils Anders Danielsson for this example.)
sized codata Stream (+ A : Set) : Size -> Set {
  cons : (i : Size) -> A -> Stream A i -> Stream A ($ i)
}

cofun map2 : (i : Size) -> (Nat -> Nat) -> Stream Nat i -> Stream Nat i 
{
map2 .($ ($ i)) f (cons .Nat .($ i) u (cons .Nat i x xl)) = 
  cons Nat _ (f u) (cons Nat _ (f x) (map2 _ f xl))
}
The type of map2 promises if you give me a stream which can be consumed to at least depth i, I return you a stream with the same guarantee. Returning a stream of guaranteed depth 0 is never a problem, since that is a contentless promise (like I promise to give you 0 EUR). But the code of map2 fails to fulfill the promise for depth 1. Given a stream of depth 1 only, it diverges when trying to match to depth 2, instead of returning a stream of depth 1.

Consequently, MiniAgda rejects map2. Technically, this is realized by only accepting dot-patterns for the principal size argument of a coinductive constructor. This makes sense, because in order to match coinductive data, I need to know beforehand that it is guarded, meaning that is has non-zero depth. Thus, I cannot just try to match like for inductive data, because matching coinductive data triggers evaluation which might not return if it fails to produce a guard.

Thus, an attempt to define map2 needs to look like:
cofun map2 : (i : Size) -> (Nat -> Nat) -> Stream Nat i -> Stream Nat i 
{
map2 ($ ($ i)) f (cons .Nat .($ i) u (cons .Nat .i x xl)) = 
  cons Nat _ (f u) (cons Nat _ (f x) (map2 _ f xl))
}
Now, we are matching on the input size using pattern $ ($ i). It is clear that this is not a complete match, since the size could be just 1, then, there is no matching clause. Consequently this is also rejected in MiniAgda. Only the size pattern $ i is accepted. Matching to depth 2 would require the type Stream Nat (2i) -> Stream Nat (2i) but MiniAgda does not support it (although such an extension is thinkable).

For deep coinductive matching, one can use case i { ($ j) -> ... }. Such a case (as the pattern ($ i)) is legal when constructing a term whose type ends in a codata type with depth i. This is sound since the case i = 0 is an empty promise which is trivially fulfilled. The only other case is nonzero depth which can be handled by a successor pattern.
cofun fib : (i : Size) -> Stream Nat i
{
  fib i = case i
   { ($ j) -> cons Nat j 0 (case j 
   { ($ k) -> cons Nat k 1 (zipWith Nat Nat Nat add k 
                              (fib k) 
                              (tail Nat k (fib ($ k))))})}
}
Here the case i is ok since we are producing a Stream Nat i. Inside the first coconstructor cons Nat j 0 ... we a producing a Stream Nat j. Thus, we can case j. Under the two constraints i > j and j > k the two recursive calls to fib type-check!

Usually, the $ i pattern is sufficient and case can be avoided.
cofun zipWith : (A : Set) -> (B : Set) -> (C : Set) ->
                (A -> B -> C) -> (i : Size) ->
		Stream A i -> Stream B i -> Stream C i 
{
  zipWith A B C f ($ i) (cons .A .i a as) (cons .B .i b bs) = 
	cons C i (f a b)  (zipWith A B C f i as bs) 
}

Correct deep matching

2010-03-12: CORIAS meeting in Val d'Ajol (thanks to Cody Roux for getting me invited and to Gilles Dowek for inviting me). Solved the treatment of deep matching. When matching against a variable x : D i of sized type D i with constructor c : [j : Size] -> D j -> D ($ j) we do not instantiate i to $ j but add the constraint i > j instead.
data Nat : Set
{ zero : Nat
; succ : Nat -> Nat
}

sized data Ord : Size -> Set
{ ozero : [i : Size] -> Ord ($ i)
; osucc : [i : Size] -> Ord i -> Ord ($ i)
; olim  : [i : Size] -> (Nat -> Ord i) -> Ord ($ i)
}

fun idO : [i : Size] -> Ord i -> Ord i
{ idO i (ozero (i > j)  ) = ozero j
; idO i (osucc (i > j) p) = osucc j (idO j p)
; idO i (olim  (i > j) f) = olim  j (\ n -> idO j (f n))
} 
(i > j) is a new size pattern that matches size variable j against the actual size, recording the constraint i > j for type checking. The counterexample below cannot be replayed with these size patterns. The maximum function can still be precisely typed using a max on sizes.
sized data Nat : Size -> Set
{ zero : [i : Size] -> Nat ($ i)
; succ : [i : Size] -> Nat i -> Nat ($ i)
}

fun maxN : [i : Size] -> Nat i -> Nat i -> Nat i 
{ maxN i (zero (i > j)  ) (zero (i > k)  ) = zero j
; maxN i (zero (i > j)  ) (succ (i > k) m) = succ k m
; maxN i (succ (i > j) n) (zero (i > k)  ) = succ j n
; maxN i (succ (i > j) n) (succ (i > k) m) = succ (max j k) 
                                            (maxN (max j k) n m)
}

Non-termination with deep matching

2010-02-02: With Cody Roux I found the following counterexample to termination checking with deep matching.
data Nat : Set
{ zero : Nat
; succ : Nat -> Nat
}

sized data O : Size -> Set
{ Z : [i : Size] -> O ($ i)
; S : [i : Size] -> O i -> O ($ i)
; L : [i : Size] -> (Nat -> O i) -> O ($ i)
; M : [i : Size] -> O i -> O i -> O ($ i)
}

fun emb : Nat -> O #
{ emb zero = Z #
; emb (succ n) = S # (emb n)
}

let pre : [i : Size] -> (Nat -> O ($$ i)) -> Nat -> O ($ i)
  = \ i -> \ f -> \ n -> case (f (succ n))
    { (Z .($ i))   -> Z i
    ; (S .($ i) x) -> x
    ; (L .($ i) g) -> g n
    ; (M .($ i) a b) -> a
    } 

fun deep : [i : Size] -> O i -> Nat -> Nat
{ deep .($$$$ i) (M .($$$ i) 
                    (L .($$ i) f) 
                    (S .($$ i) (S .($ i) (S i x))))  n
  = deep _ (M _ (L _ (pre _ f)) (S _ (f n))) (succ (succ (succ n)))
; deep i x n = n   
}

let four : Nat 
  = succ (succ (succ (succ zero)))

eval let loop : Nat = deep # (M # (L # emb) (emb four)) four
The pattern (L .($$ i) f) in deep is the problem. The correct pattern is (L .i f). By subtyping these two terms are both of the required type O ($$$ i), but the least size must be chosen to be on the safe side. Thus, the implementation of dot patterns has to be changed to account for subtyping.

Forced matching

2010-01-21: A partial interpreter for untyped lambda calculus with a termination proof in the style of Bove/Capretta.
data Nat : Set 
{ zero : Nat
; succ : Nat -> Nat
}

data List (+A : Set) : Set
{ nil  : List A
; cons : A -> List A -> List A
}

-- de Bruijn terms

data Exp : Set
{ var : Nat -> Exp
; abs : Exp -> Exp 
; app : Exp -> Exp -> Exp
}

-- set of values

data D : Set
{ clos : Exp -> (List D) -> D
}

-- environment operations

let Env : Set
      = List D

let empty : Env
      = nil D

let update : Env -> D -> Env
      = \ rho -> \ d -> cons D d rho       

let dummy : D
          = clos (var zero) empty

fun lookup : Env -> Nat -> D
{ lookup (nil .D) n = dummy
; lookup (cons .D d rho) zero = d
; lookup (cons .D d rho) (succ n) = lookup rho n
}

-- inductive graph of the evaluation function

data Eval : Exp -> Env -> D -> Set
{ evVar : (k : Nat) -> (rho : Env) ->  
          Eval (var k) rho (lookup rho k)
; evAbs : (e : Exp) -> (rho : Env) -> 
          Eval (abs e) rho (clos e rho)  
; evApp : (f : Exp) -> (e : Exp) -> (rho : Env) -> 
          (f' : Exp) -> (rho' : Env) -> (d : D) -> (d' : D) -> 
          Eval f rho (clos f' rho') ->
          Eval e rho d ->
          Eval f' (update rho' d) d' ->
          Eval (app f e) rho d'
}

-- evaluation as a partial function
{- after erasure, the function will take the form

    evaluate : Exp -> Env -> D
-}

mutual {

  fun evaluate : (e : Exp) -> (rho : Env) -> 
                 [d : D] -> [Eval e rho d] -> 
  { evaluate (var k) rho .(lookup rho k) (evVar .k .rho) = lookup rho k
  ; evaluate (abs e) rho .(clos e rho)   (evAbs .e .rho) = clos e rho
  ; evaluate (app f e) rho .d' (evApp .f .e .rho f' rho' d d' evF evE evF')
      = apply f' rho' (evaluate f rho (clos f' rho') evF)
                      (evaluate e rho d evE)  d' evF'
  }

  fun apply : [f' : Exp] -> [rho' : Env] ->  -> 
              (d : D) -> [d' : D] -> [Eval f' (update rho' d) d'] ->  
  { apply .f' .rho' (clos f' rho') d d' p = evaluate f' (update rho' d) d' p  
  }
}
Note that in evaluate we match against [Eval e rho d] even though it is erased. It is possible since there is only one matching constructor.

Counting constructors in termination checking

2010-01-14: Now the following code is accepted.
data Nat : Set 
{ zero : Nat
; succ : Nat -> Nat
}

mutual {
  fun f : Nat -> Nat
  { f zero = zero
  ; f (succ zero) = zero
  ; f (succ (succ n)) = g n
  }

  fun g : Nat -> Nat
  { g zero = zero
  ; g (succ n) = f (succ (succ n))
  }
}
Since f takes off two constructors before calling g, g might put one back before calling f without jeopardizing termination. This is especially useful in combination with sized types. It makes the following implementation of merge termination-check.
data Bool : Set
{ true  : Bool
; false : Bool
}

data Nat : Set
{ zero : Nat
; suc  : Nat -> Nat
}

sized data List : Size -> Set
{ nil  : (i : Size) -> List ($ i)  
; cons : (i : Size) -> Nat -> List i -> List ($ i)
}

fun leq : Nat -> Nat -> Bool {}

-- merge as would be represented with "with" in Agda
mutual {
  fun merge : (i : Size) -> List i -> (j : Size) -> List j -> List #
  { merge .($ i) (nil i) j l = l
  ; merge i l .($ j) (nil j) = l
  ; merge .($ i) (cons i x xs) .($ j) (cons j y ys) = merge_aux i x xs j y ys (leq x y)
  }
  fun merge_aux : (i : Size) -> Nat -> List i -> (j : Size) -> Nat -> List j -> Bool -> List #
  { merge_aux i x xs j y ys true  = cons # x (merge i xs ($ j) (cons j y ys))
  ; merge_aux i x xs j y ys false = cons # y (merge ($ i) (cons i x xs) j ys) 
  }
}

Inconsistency from injective data type constructors

2010-01-12: This is an implementation of Chung-Kil Hur's and Hugo Herbelin's derivation of absurdity. It makes use of fancy case.
data Empty : Set {}

data Unit : Set
{ unit : Unit
}

data Or (A : Set) (B : Set) : Set
{ inl : A -> Or A B
; inr : B -> Or A B
}

data Eq (A : Set)(a : A) : A -> Set
{ refl : Eq A a a
} 

fun cong : (F : Set -> Set) -> (G : Set -> Set) -> (A : Set) ->
  Eq (Set -> Set) F G -> Eq Set (F A) (G A)
{ cong F .F A (refl .(Set -> Set) .F) = refl Set (F A)
} 

fun castLR : (A : Set) -> (B : Set) -> Eq Set A B -> A -> B
{ castLR A .A (refl .Set .A) a = a
}

fun castRL : (A : Set) -> (B : Set) -> Eq Set A B -> B -> A
{ castRL A .A (refl .Set .A) a = a
}

data I (F : Set -> Set) : Set {}

fun injI : (F : Set -> Set) -> (G : Set -> Set) -> Eq Set (I F) (I G) -> Eq (Set -> Set) F G
{ injI F .F (refl .Set .(I F)) = refl (Set -> Set) F
}
 
data InvI (A : Set) : Set
{ inv : (X : Set -> Set) -> Eq Set (I X) A -> InvI A
} 

let EM : Set 
       = (A : Set) -> Or A (A -> Empty)

fun em : EM {}  -- postulate excluded middle

fun cantor : Set -> Set
{ cantor A = case (em (InvI A)) 
  { (inl .(InvI A) .(InvI A -> Empty) (inv .A X p)) -> X A -> Empty
  ; (inr .(InvI A) .(InvI A -> Empty) bla) -> Unit
  }
} 

{- now define (modulo casts and irrelevant cases)

   no  = \ f -> f f
   yes = \ f -> f f
-}

let no : cantor (I cantor) -> Empty
= \ f -> case (em (InvI (I cantor)))
  { (inl .(InvI (I cantor)) .(InvI (I cantor) -> Empty) 
      (inv .(I cantor) X p)) -> 
        f (castRL (X (I cantor)) 
                  (cantor (I cantor)) 
                  (cong X cantor (I cantor) (injI X cantor p)) 
                  f)
  ; (inr .(InvI (I cantor)) .(InvI (I cantor) -> Empty) g) ->
      g (inv (I cantor) cantor (refl Set (I cantor)))   
  }


let yes : cantor (I cantor)
= case (em (InvI (I cantor)))
  { (inl .(InvI (I cantor)) .(InvI (I cantor) -> Empty) 
      (inv .(I cantor) X p)) -> 
        \ f -> (castLR (X (I cantor)) 
                  (cantor (I cantor)) 
                  (cong X cantor (I cantor) (injI X cantor p)) 
                  f) f
  ; (inr .(InvI (I cantor)) .(InvI (I cantor) -> Empty) g) -> unit
  }


eval let omega : Empty
          = no yes

"Resurrection" of Irrelevant Erased Parts

data Sigma (A : Set) (B : A -> Set) : Set
{ pair : (fst : A) -> (snd : B fst) -> Sigma A B
}

data Nat : Set
{ zero : Nat
; succ : Nat -> Nat
}

data Empty : Set
{
}

-- eliminator for Empty: zero cases
fun abort : (A : Set) -> Empty -> A
{ 
}

-- magic is ok, since all inhabitants of Empty are equal
let magic : (A : Set) -> [Empty] -> A
          = \ A -> \ p -> abort A p

data Unit : Set
{ unit : Unit
}

fun Vec : (A : Set) -> (n : Nat) -> Set
{ Vec A zero     = Empty
; Vec A (succ n) = Sigma A (\ z -> Vec A n)
}

fun Leq : (n : Nat) -> (m : Nat) -> Set
{ Leq  zero     m        =  Unit
; Leq (succ n)  zero     =  Empty
; Leq (succ n) (succ m)  =  Leq n m
}

-- lookup A n m p v  does not depend on the proof p : m < n
fun lookup : (A : Set) -> (n : Nat) -> (m : Nat) -> [Leq (succ m) n] -> Vec A n -> A
{ lookup A  zero    m        p v = abort A p
; lookup A (succ n) zero     p v = fst A (\ z -> Vec A n) v
; lookup A (succ n) (succ m) p v = lookup A n m p (snd A (\ z -> Vec A n) v)
}

Eta-expansion for Propositional Equality

data Id (A : Set) (a : A) : A -> Set 
{ refl : Id A a a 
}

fun subst : (A : Set) -> (a : A) -> (b : A) -> Id A a b -> 
  (P : A -> Set) -> P a -> P b
{ subst A a .a (refl .A .a) P x = x
}

-- this demonstrates eta expansion at the identity type
let bla :  (A : Set) -> (a : A) -> (p : Id A a a) -> 
           (P : A -> Set) -> (x : P a) -> 
              Id (P a) x (subst A a a p P x)
        =  \ A -> \ a -> \ p -> \ P -> \ x -> refl (P a) x

Case over Bool

data Nat : Set 
{ zero : Nat
; suc  : Nat -> Nat
}

data Bool : Set
{ true  : Bool
; false : Bool 
}

fun leq : Nat -> Nat -> Bool
{ leq zero n = true
; leq (suc m) zero = false
; leq (suc m) (suc n) = leq m n
}

data Id (A : Set) (a : A) : A -> Set
{ refl : Id A a a
}

fun True : Bool -> Set
{ True b = Id Bool b true
}
let triv : True true
         = refl Bool true

fun False : Bool -> Set
{ False b = Id Bool b false
}
let triv' : False false
          = refl Bool false

fun leFalse : (n : Nat) -> (m : Nat) -> False (leq n m) -> True (leq m n)
{ leFalse  n       zero   p = triv
; leFalse (suc n) (suc m) p = leFalse n m p
-- ; leFalse zero (suc m) () -- IMPOSSIBLE
}

data SList : Nat -> Set
{ snil  : SList zero
; scons : (m : Nat) -> (n : Nat) -> True (leq n m)  -> SList n -> SList m
} 

fun max : Nat -> Nat -> Nat
{ max n m = case leq n m 
  { true -> m
  ; false -> n
  }
}

fun maxLemma : (n : Nat) -> (m : Nat) -> (k : Nat) ->
              True (leq n k) -> True (leq m k) -> True (leq (max n m) k)
{ maxLemma n m k p q = case leq n m 
  { true  -> q
  ; false -> p
  } 
}

fun insert : (m : Nat) -> (n : Nat) -> SList n -> SList (max n m)
{ insert m .zero snil = scons m zero triv snil
; insert m .n (scons n k p l) = case leq n m 
  { true  -> scons m n triv (scons n k p l)
  ; false -> scons n (max k m) (maxLemma k m n p (leFalse n m triv')) 
                   (insert m k l)
  }
}

Sized coinductive types

This is a MiniAgda implementation of the hamming stream which is productive by definition.

-- Nat ---------------------------------------------------------------

data Nat : Set 
{
  zero : Nat;
  succ : Nat -> Nat 
}

fun add : Nat -> Nat -> Nat 
{
  add  zero    = \y -> y;
  add (succ x) = \y -> succ (add x y)
}

let double : Nat -> Nat
           = \ n -> add n n
let triple : Nat -> Nat
           = \ n -> add n (double n)

fun leq : Nat -> Nat -> (C : Set) -> C -> C -> C
{
  leq  zero     y       C tt ff = tt;
  leq (succ x)  zero    C tt ff = ff;
  leq (succ x) (succ y) C tt ff = leq x y C tt ff 
}

-- Stream ------------------------------------------------------------

sized codata Stream (+ A : Set) : Size -> Set 
{
  cons : (i : Size) -> A -> Stream A i -> Stream A ($ i)
}

cofun map : (A : Set) -> (B : Set) -> (i : Size) -> 
            (A -> B) -> Stream A i -> Stream B i 
{
  map .A B ($ i) f (cons A .i x xl) = cons B _ (f x) (map A B _ f xl)
}

cofun merge : (i : Size) -> Stream Nat i -> Stream Nat i -> Stream Nat i
{
  merge ($ i) (cons .Nat .i x xs) (cons .Nat .i y ys) = 
      leq x y (Stream Nat _)
         (cons Nat _ x (merge _ xs (cons Nat _ y ys)))
	 (cons Nat _ y (merge _ (cons Nat _ x xs) ys))     
}


-- Hamming function --------------------------------------------------

cofun ham : (i : Size) -> Stream Nat i
{
  ham ($ i) = cons Nat _ (succ zero) 
                (merge i (map Nat Nat i double (ham i)) 
                         (map Nat Nat i triple (ham i)))
}


Valid HTML 4.01! Andreas Abel, http://www.tcs.ifi.lmu.de/~abel/miniagda/
Last modified: Wed Jul 1 13:57:19 CEST 2009
Valid CSS!