8.16.0.4
| (data type-signature | | maybe-prefix-form | | clause ...) |
|
| |
| type-signature | | = | | type-name | | | | | | | (type-name type-variable ...) | | | | | | | | maybe-prefix-form | | = | | #:prefix | | | | | | | #:prefix prefix-id | | | | | | | | clause | | = | | [name param ...] | | | | | | | | param | | = | | type | | | | | | | [param-name type] |
|
Just like the data type you would see in Haskell and ML, which supports parametric polymorphism. The prefix form is for namespacing the constructor of data type. The following is a normal usage, the constructors are all without namespacing.
| (data expr |
| [Var (name : Symbol)] |
| [abs (name : Symbol) (body : expr)] |
| [app (fn : expr) (arg : expr)] |
| [pi (name : Symbol) (e : expr) (body : expr)] |
| [type (level : Integer)] |
| [nat] |
| [zero] |
| [succ (n : expr)] |
| [rec expr expr expr expr] |
| [id expr expr expr] |
| [refl expr] |
| [J expr expr expr expr expr expr]) |
To have namespacing prefix, use the following code. The data type still Expr here, but the constructors will get E: prefix automatically.
| (data Expr #:prefix E |
| [Int Integer] |
| [Add Expr Expr]) |
| |
| (: Eval : Expr -> Integer) |
| (define (Eval e) |
| (match e |
| [(E:Int v) v] |
| [(E:Add l r) (+ (Eval l) (Eval r))])) |
| |
| (Eval (E:Add (E:Int 1) (E:Int 2))) |
And if you require #:prefix but didn’t provide an identifier, it will use data type LIST as prefix.
| (data (LIST T) #:prefix |
| [Nil] |
| [Cons T (LIST T)]) |
| |
| (: Len : (∀ (T) (LIST T) -> Natural)) |
| (define (Len L) |
| (match L |
| [(LIST:Nil) 0] |
| [(LIST:Cons t Tail) (add1 (Len Tail))])) |
| |
| (Len (LIST:Cons #t (LIST:Nil))) |