3.2 Sugar

8.12

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.

(require cur/stdlib/sugar)

package: cur-lib

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))))
eval:1:0: ->: expected one of these literal symbols: `Π',
`Pi', `∀', or `forall'
  at: ->
  in: (-> Type Type Type)
> ((((conj Bool) Bool) true) false)
conj: unbound identifier in module

Examples:

> (data And : 2 (forall Type Type Type)
(conj : (forall (A : Type) (B : Type) A B (And A B))))
eval:3:0: forall: bad syntax
in: (forall Type Type Type)
> ((((conj Bool) Bool) true) false)
conj: unbound identifier in module

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)
#<procedure>
> ((lambda (x : Bool) (y : Bool) y) true)
#<procedure>

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))))
eval:7:0: ->: expected one of these literal symbols: `Π',
`Pi', `∀', or `forall'
  at: ->
  in: (-> Type Type Type)
> (conj Bool Bool true false)
conj: unbound identifier in module

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))
:: unbound identifier in module
> (define (id A a) a)
<pkgs>/cur-lib/cur/curnel/coc-saccharata.rkt:107:17: λ: no
expected type, add annotations
  at: (λ A (λ/c- a a))
  in: (λ A (λ/c- a a))
  parsing context:
   while parsing has-expected-type
    term: (λ A (λ/c- a a))
    location:
<pkgs>/cur-lib/cur/curnel/coc-saccharata.rkt:107:17

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])
eval:11:0: match: expected one of these literals: #:return,
#:in, #:as, or #:with-indices
  at: (z true)
  in: (match z (z true) ((s (n : Nat)) false))

Example:

> (match z
    [(s n)
     false]
     [z true])
eval:12:0: match: expected one of these literals: #:return,
#:in, #:as, or #:with-indices
  at: ((s n) false)
  in: (match z ((s n) false) (z true))

Example:

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

Example:

> (define (+ (n : Nat) (m : Nat))
    (match n
      [z m]
      [(s n) (s (+ n m))]))
eval:14:0: match: expected one of these literals: #:return,
#:in, #:as, or #:with-indices
  at: (z m)
  in: (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: expected one of these literals: #:return,
#:in, #:as, or #:with-indices
  at: (nil (lambda (n : Nat) (none A)))
  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: unbound identifier in 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)
::: unbound identifier in module
> (:: true Nat)
::: unbound identifier in module

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)
run: unbound identifier in module

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))
step: unbound identifier in module

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))
step-n: unbound identifier in module

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)
query-type: unbound identifier in module

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

3.1	Datum
3.2	Sugar
3.3	Bool
3.4	Nat
3.5	Dependent Pairs
3.6	Maybe
3.7	List
3.8	Equality
3.9	ASCII
3.10	Racket ASCII
3.11	Typeclass