▼Cur
On this page:
Type
λ
#%app
Π
data
elim
new-elim
define
cur-axiom
void
8.16.0.1
  top  contents    up   

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))
> ((λ (x : Bool) x) true)

(true)

> (data False : 0 (Type 0))
> (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)))))))
> ((((conj Bool) Bool) true) false)

(conj (Bool) (Bool) (true) (false))

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)))
> (elim Nat (λ (x : Nat) Nat)
        (z
         (λ (n : Nat) (λ (IH : Nat) n)))
        (s z))

(z)

> (elim And (λ (_ : ((And Nat) Bool)) ((And Bool) Nat))
        ((λ (n : Nat)
          (λ (b : Bool)
            ((((conj Bool) Nat) b) n))))
        ((((conj Nat) Bool) z) true))

(conj (Bool) (Nat) (true) (z))

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)))
> (define sub1 (λ (n : Nat)
                 (elim Nat (λ (x : Nat) Nat)
                       (z
                        (λ (n : Nat) (λ (IH : Nat) n)))
                       n)))
> (sub1 (s (s z)))

(s (z))

> (sub1 (s z))

(z)

> (sub1 z)

(z)

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.

  top  contents    up