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 |
Changed in version 0.20 of package cur-lib: Moved Type synonym from Curnel.
syntax
(-> decl decl ... type)
decl = type | (identifier : type)
> (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))
> (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)
> ((lambda (x : Bool) (lambda (y : Bool) y)) true) (...impl/runtime.rkt:231:31 (Bool) #<procedure:...impl/runtime.rkt:231:31>)
> ((lambda (x : Bool) (y : Bool) y) true) (...impl/runtime.rkt:231:31 (Bool) #<procedure:...impl/runtime.rkt:231:31>)
syntax
(#%app f a ...)
> (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)
syntax
(define-type name type)
(define-type (name (a : t) ...) body)
syntax
(match e [maybe-in] [maybe-return] [pattern body] ...)
maybe-in = #:in type maybe-return = #:return type pattern = constructor | (constructor x ...) | (constructor (x : t) ...)
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.
> ((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)
syntax
(let (clause ...) body)
clause = (id expr) | ((id : type) expr)
> (let ([x Type] [y (λ (x : (Type 1)) x)]) (y x)) (Type 0)
> (let ([x uninferrable-expr] [y (λ (x : (Type 1)) x)]) (y x)) type:uninferrable-expr: undefined;
cannot reference an identifier before its definition
in module: 'anonymous-module
syntax
(:: e type)
> (:: 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)
> (lambda (x : (run (if true Bool Nat))) x) (...impl/runtime.rkt:231:31 (Bool) #<procedure:...impl/runtime.rkt:231:31>)
syntax
(step syn)
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)
> (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)
> (query-type Bool) "Bool" has type "(typed-Type 0)"