On this page:
Type
->
forall
Pi
Π
lambda
λ
#%app
:
define
define-type
match
recur
let
:  :
run
step
step-n
query-type
7.1

3.2 Sugar

The curnel forms are sort of terrible for actually writing code. Functions and applications are limited to single artity. Functions type must be specified using the dependent forall, even when the dependency is not used. Inductive elimination can only be done via the primitive eliminator and not via pattern matching. However, with the full force of Racket’s syntactic extension system, we can define not only simply notation, but redefine what application means, or define a pattern matcher that expands into the eliminator.

This library defines various syntactic extensions making Cur easier to write than writing raw TT.

syntax

(Type n)

Type
Added Type as a synonym for (Type 0).

Changed in version 0.20 of package cur-lib: Moved Type synonym from Curnel.

syntax

(-> decl decl ... type)

 
decl = type
  | (identifier : type)
A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying. Also exported as the following names, because there are lots of synonyms in the literature: , forall, , Pi, Π.

Examples:
> (data And : 2 (-> Type Type Type)
    (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
> ((((conj Bool) Bool) true) false)

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

Examples:
> (data And : 2 (forall Type Type Type)
    (conj : (forall (A : Type) (B : Type) A B (And A B))))
> ((((conj Bool) Bool) true) false)

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

syntax

(lambda (a : t) ... body)

Defines a multi-arity procedure that supports automatic currying. Also provied as λ.

Examples:
> ((lambda (x : Bool) (lambda (y : Bool) y)) true)

(...impl/runtime.rkt:229:31 (Bool) #<procedure:...impl/runtime.rkt:229:31>)

> ((lambda (x : Bool) (y : Bool) y) true)

(...impl/runtime.rkt:229:31 (Bool) #<procedure:...impl/runtime.rkt:229:31>)

syntax

(#%app f a ...)

Defines multi-arity procedure application via automatic currying.

Examples:
> (data And : 2 (-> Type Type Type)
    (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
> (conj Bool Bool true false)

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

syntax

(: name type)

Declare that the function which will be defined as name has type type. Must precede the definition of name. type must expand to a function type of the form (Π (x : t1) t2) When used, this form allows omitting the annotations on arguments in the definition name

syntax

(define name body)

(define (name x ...) body)
(define (name (x : t) ...) body)
Like the define provided by cur, but supports defining curried functions via lambda. The second form, (define (name x ...) body), can only be used when a (: name type) form appears earlier in the module. Also record name in the transformer environment.

Examples:
> (: id (forall (A : Type) (a : A) A))
> (define (id A a) a)

syntax

(define-type name type)

(define-type (name (a : t) ...) body)
Like define, but uses forall instead of lambda.

syntax

(match e [maybe-in] [maybe-return] [pattern body] ...)

 
maybe-in = #:in type
     
maybe-return = #:return type
     
pattern = constructor
  | (constructor x ...)
  | (constructor (x : t) ...)
A pattern-matcher for inductive types. Match clauses must begin with the constructor name, and be followed by all indices and constructor arguments as pattern variable. Match clauses can be given in any order.

Pattern variables do not need to be annotated, as the ‘match‘ form can infer their types. If pattern variables are annotated, then the ‘match‘ form will ensure the annotation matches the expected type before elaborating.

If ‘match‘ is used under a ‘define‘, ‘match‘ can be used to define simple primitive recursive functions, defined by induction on their first argument.

Inside the body, recur can be used to refer to the inductive hypotheses for an inductive argument. Generates a call to the inductive eliminator for e. Currently does not work on inductive type-families as types indices are not inferred.

If #:in is not specified, attempts to infer the type of e. If #:return is not specified, attempts to infer the return type of the match.

Example:
> (match z
    [z true]
    [(s (n : Nat))
     false])

(true)

Example:
> (match z
    [(s n)
     false]
     [z true])

(true)

Example:
> (match (s z)
    #:in Nat
    #:return Bool
    [z true]
    [(s n)
    (not (recur n))])

(false)

Example:
> (define (+ (n : Nat) (m : Nat))
    (match n
      [z m]
      [(s n) (s (+ n m))]))

Example:
> ((match (nil Bool)
    [nil
     (lambda (n : Nat)
       (none A))]
    [(cons (a : Bool) (rest : (List Bool)))
     (lambda (n : Nat)
       (match n
         [z (some Bool a)]
         [(s (n-1 : Nat))
          ((recur rest) n-1)]))])
   z)

eval:15:0: match: Could not infer return type. Try using

#:return to declare it.

  in: (match (nil Bool) (nil (lambda (n : Nat) (none A)))

((cons (a : Bool) (rest : (List Bool))) (lambda (n : Nat)

(match n (z (some Bool a)) ((s (n-1 : Nat)) ((recur rest)

n-1))))))

syntax

(recur id)

A form valid only in the body of a match clause. Generates a reference to the induction hypothesis for x inferred by a match clause.

syntax

(let (clause ...) body)

 
clause = (id expr)
  | ((id : type) expr)
Evaluates the expressions expr from each clause, left to right, and binds them to each id. If a type is not given for the id, attempts to infer the type of the corresponding expr, raising a syntax error if no type can be inferred.

Examples:
> (let ([x Type]
        [y (λ (x : (Type 1)) x)])
    (y x))

(Type 0)

> (let ([x uninferrable-expr]
        [y (λ (x : (Type 1)) x)])
    (y x))

uninferrable-expr: undefined;

 cannot reference an identifier before its definition

  in module: 'anonymous-module

syntax

(:: e type)

Check that expression e has type type, causing a type-error if not, and producing (void) if so.

Examples:
> (:: z Nat)
> (:: true Nat)

eval:19:0: ::: Term true does not have expected type Nat.

Inferred type was Bool

  in: (:: true Nat)

syntax

(run syn)

Like cur-normalize, but is a syntactic form to be used in surface syntax. Allows a Cur term to be written by computing part of the term from another Cur term.

Example:
> (lambda (x : (run (if true Bool Nat))) x)

(...impl/runtime.rkt:229:31 (Bool) #<procedure:...impl/runtime.rkt:229:31>)

syntax

(step syn)

Like run, but uses cur-step to evaluate only one step and prints intermediate results before returning the result of evaluation.

Example:
> (step (plus z z))

Warning: cur-step is not yet supported.

z

(z)

Changed in version 0.20 of package cur-lib: Broken by new Curnel; fix is part of planned rewrite of evaluator.

syntax

(step-n natural syn)

Like step, but expands to natural calls to step.

Example:
> (step-n 3 (plus z z))

Warning: cur-step is not yet supported.

Warning: cur-step is not yet supported.

Warning: cur-step is not yet supported.

z

z

z

(z)

Changed in version 0.20 of package cur-lib: Broken by new Curnel; fix is part of planned rewrite of evaluator.

syntax

(query-type expr)

Print the type of expr, at compile-time. Similar to Coq’s Check.

Example:
> (query-type Bool)

"Bool" has type "(typed-Type 0)"