1 Curnel Forms

8.6

1 Curnel Forms

Curnel forms are the core forms provided cur. These forms come directly from the trusted core and are all that remain after macro expansion. TODO: Link to guide regarding macro expansion The core of cur is essentially TT with an impredicative universe (Type 0). For a very understandable in-depth look at TT, see chapter 2 of Practical Implementation of a Dependently Typed Functional Programming Language, by Edwin C. Brady.

syntax
(Type n)

Define the universe of types at level n, where n is any natural number. Cur is impredicative in (Type 0), although this is likely to change to a more restricted impredicative universe.

Examples:

> (Type 0)
(Type- 0)
> (Type 1)
(Type- 1)

Changed in version 0.20 of package cur-lib: Removed Type synonym from Curnel; changed run-time representation from symbolic '(Unv n) to transparent struct.

syntax
(λ (id : type-expr) body-expr)

Produces a single-arity procedure, binding the identifier id of type type-expr in body-expr and in the type of body-expr. Both type-expr and body-expr can contain non-curnel forms, such as macros.

Currently, Cur will return the underlying representation of a procedure when a λ is evaluated at the top-level. Do not rely on this representation.

Examples:

> (λ (x : (Type 0)) x)
#<procedure>
> (λ (x : (Type 0)) (λ (y : x) y))
#<procedure>

Changed in version 0.20 of package cur-lib: Changed run-time representation from symbolic '(λ (x : t) e) to Racket procedure

syntax
(#%app procedure argument)

Applies the single-arity procedure to argument.

Examples:

> ((λ (x : (Type 1)) x) (Type 0))
(Type- 0)
> (#%app (λ (x : (Type 1)) x) (Type 0))
(Type- 0)

syntax
(Π (id : type-expr) body-expr)

Produces a dependent function type, binding the identifier id of type type-expr in body-expr.

Examples:

> (Π (x : (Type 0)) (Type 0))
(Π-- (Type- 0) #<procedure:.../cur/curnel/coc.rkt:61:47>)
> (λ (x : (Π (x : (Type 1)) (Type 0)))
(x (Type 0)))
#<procedure>

Changed in version 0.20 of package cur-lib: Changed run-time representation from symbolic '(Π (x : t) e) to a transparent struct.

syntax
(data id : nat type-expr (id* : type-expr*) ...)

Defines an inductive datatype named id of type type-expr whose first nat arguments are parameters, with constructors id* each with the corresponding type type-expr*.

Examples:

> (data Bool : 0 (Type 0)
        (true : Bool)
        (false : Bool))
inspector-superior?: contract violation
  expected: inspector?
  given: #f
> ((λ (x : Bool) x) true)
Bool: unbound identifier in module
> (data False : 0 (Type 0))
inspector-superior?: contract violation
  expected: inspector?
  given: #f
> (data And : 2 (Π (A : (Type 0)) (Π (B : (Type 0)) (Type 0)))
    (conj : (Π (A : (Type 0)) (Π (B : (Type 0)) (Π (a : A) (Π (b : B) ((And A) B)))))))
inspector-superior?: contract violation
  expected: inspector?
  given: #f
> ((((conj Bool) Bool) true) false)
conj: unbound identifier in module

Changed in version 0.20 of package cur-lib: Added strict positivity checking. (or, at least, documented it)

syntax
(elim inductive-type motive (method ...) target)

Fold over the term target of the inductively defined type inductive-type. The motive is a function that expects the indices of the inductive type and a term of the inductive type and produces the type that this fold returns. The type of target is (inductive-type index ...). elim takes one method for each constructor of inductive-type. Each method expects the arguments for its corresponding constructor, and the inductive hypotheses generated by recursively eliminating all recursive arguments of the constructor.

The following example runs (sub1 (s z)).

Examples:

> (data Nat : 0 (Type 0)
    (z : Nat)
    (s : (Π (n : Nat) Nat)))
inspector-superior?: contract violation
  expected: inspector?
  given: #f
> (elim Nat (λ (x : Nat) Nat)
        (z
         (λ (n : Nat) (λ (IH : Nat) n)))
        (s z))
elim-Nat: unbound identifier in module
> (elim And (λ (_ : ((And Nat) Bool)) ((And Bool) Nat))
        ((λ (n : Nat)
          (λ (b : Bool)
            ((((conj Bool) Nat) b) n))))
        ((((conj Nat) Bool) z) true))
elim-And: unbound identifier in module

NOTE: This function is deprecated; use new-elim, instead.

syntax
(new-elim target motive (method ...))

Like elim, but makes the type annotation unnecessary.

Added in version 0.20 of package cur-lib.

syntax
(define id expr)

Binds id to the result of expr.

Examples:

> (data Nat : 0 (Type 0)
    (z : Nat)
    (s : (Π (n : Nat) Nat)))
inspector-superior?: contract violation
  expected: inspector?
  given: #f
> (define sub1 (λ (n : Nat)
                 (elim Nat (λ (x : Nat) Nat)
                       (z
                        (λ (n : Nat) (λ (IH : Nat) n)))
                       n)))
Nat: unbound identifier in module
> (sub1 (s (s z)))
sub1: unbound identifier in module
> (sub1 (s z))
sub1: unbound identifier in module
> (sub1 z)
sub1: unbound identifier in module

syntax
(cur-axiom id : type)

Creates a new constant id of type type which has no computational content.

Added in version 0.20 of package cur-lib.

syntax
(void)

A representation of nothing. Primarily used by extensions that perform side-effects but produce nothing.

Added in version 0.20 of package cur-lib.

1	Curnel Forms
2	Reflection
3	Standard Library
4	Olly: Ott-like Librar Y
5	ntac: The New Tactic System