tur/forms/datatypes
declaring records, sums and newtypes: defstruct, defdata, defgadt, defopaque.
Four forms declare a new nominal type. defstruct is a record: all of its fields at once. defdata is a sum: one of several constructors, each with its own payload, taken apart with match; a constructor may also say what type index it produces, (Lit int : (Expr int)), so match can learn something from the arm that fired. defgadt, deprecated, is the older spelling of a defdata whose every constructor says so. defopaque is a newtype: a distinct type that is, at run time, nothing but its representation. Each introduces constructor functions with the type's name; the type name itself works as an annotation.
A type is usually declared at file scope. One written inside a function body (defstruct, defdata, defopaque) is lifted to file scope, as a nested defn is: its name is visible from that point on, and to the rest of the program.
A name that an auto-loaded stdlib module already defines (Pair, Option, ...) or that an earlier form of the file defined cannot be defined again ('Pair' is already defined by an auto-loaded stdlib module ... pick a distinct name). The copy kind decides how values are used: :copy values are reused freely (every field must itself be copyable), a :move value -- the default -- may be used once (TUR-E0201 on a second use), and a :linear one must be consumed exactly once (TUR-E0100 if dropped). structs-guide, sum-types-guide, gadts-guide and opaques-guide cover each at length.
defstruct
(defstruct Name [field : Type ...]) (defstruct Name :copy [field : Type ...]) (defstruct Name [A ...] [field : A ...])
declare a record type.
(defstruct Name [field : Type ...]) declares a record and binds Name as a constructor: (Name a b) builds one, (.field s) reads a field, and (set! (.field s) v) writes one of a ^mut binding. An annotation between the name and the fields sets the copy kind: :copy, :move (the default) or :linear; :heap keeps the value behind a pointer, so that sharing it is the point (an interior-mutable node); :no-auto-ctor stops the name being bound as a constructor when it is already a value elsewhere (use make-struct). Type parameters go in a vector before the fields, (defstruct Duo [A B] [fst : A snd : B]). A struct is passed to a function by value, so a callee that changes its parameter changes its own copy. Field types are checked at construction (expected int, got float) and an unknown field is no typeclass method found for 'y'. Field names must be distinct: [x : int x : int] is an error.
| Name | the type's name, which is also its constructor | |
| kind | optional: :copy, :move, :linear, :heap, :no-auto-ctor | |
| [A ..] -- optional type parameters | ||
| fields | [name : Type ...] |
(defstruct Point :copy [x : int y : int]) (defn sum-pt [p : Point] : int (+ (.x p) (.y p))) (sum-pt (Point 3 4)) ; => 7 ; ; doctest: a type declared inside the test body does not build when compiled
make-struct
(make-struct Name value ...) (make-struct Name :field value ...)
build a struct value, by position or by field name.
(make-struct Name v1 v2 ...) supplies every field in declaration order, as (Name v1 v2 ...) does; the count must match. (make-struct Name :y 2 :x 1) names the fields and may give them in any order. Keyword construction is strict: a missing field is TUR-E0292, an unknown one TUR-E0294, a repeated one TUR-E0293, and mixing positions with keywords TUR-E0299. A call with too few positional values is a partial application -- ((Point 5) 6) is the point (5, 6) -- which keyword calls do not do. Use make-struct for a struct declared :no-auto-ctor, or where the name Name is a value in scope.
| Name | the struct's name | |
| values | one per field, or :field value pairs |
The new struct.
(defstruct Pt2 :copy [x : int y : int]) (.x (make-struct Pt2 :y 2 :x 1)) ; => 1 ; ; doctest: a type declared inside the test body does not build when compiled (.y (make-struct Pt2 5 6)) ; => 6 ; ; doctest: a type declared inside the test body does not build when compiled
defdata
(defdata Name (Ctor payload ...) ...) (defdata Name :copy [A ...] (Ctor payload ...) ...) (defdata Name [A ...] (Ctor payload ... : Result) ...)
declare a sum type.
(defdata Name (Ctor payload ...) ...) declares a type that is one of its constructors. A payload is a keyword type ((Circle :int)), a type parameter or another type; a constructor may carry nothing, (Red). A record-style constructor names its fields, (Rect [w : int h : int]), and is built by position or by keyword, (Rect :h 4 :w 3). Type parameters follow the name in a vector, (defdata Tree [a] (Leaf) (Node (Tree a) a (Tree a))), and :copy or :move (the default) goes after the name, before or after the vector; :linear, :affine and :heap go there too. Constructors are ordinary functions, (Circle 2), and match takes a value apart: leaving a constructor out of a match is the error match: non-exhaustive patterns, which names the constructor, unless the match is marked ^non-exhaustive.
A constructor may end with : Result, the type it produces: (Lit int : (Expr int)), (Rect [w : int h : int] : (Shape int)). The result is an application of Name to as many arguments as it has parameters, and an unannotated constructor produces the generic (Name a ...). A constructor whose result fixes a parameter is refining: (IsZero ...) is an (Expr bool), passing it where an (Expr int) is wanted is TUR-E0001, a match on an (Expr int) need only list the constructors that can produce one, and inside an arm the checker knows what the parameter is. Equality proofs (Equal, Refl) are built on this (see coerce). gadts-guide has the rest.
| Name | the type's name | |
| [A ..] -- optional type parameters | ||
| (Ctor ...) -- one constructor with its payload types, or none | ||
| : Result -- optional, per constructor: the type it produces |
(defdata Shape (Circle :int) (Rect :int :int)) (defn area [s : Shape] : int (match s (Circle r) (* 3 (* r r)) (Rect w h) (* w h))) (area (Rect 3 4)) ; => 12 ; ; doctest: a type declared inside the test body does not build when compiled (defdata Expr [a] (Lit int : (Expr int)) (IsZero (Expr int) : (Expr bool)) (If (Expr bool) (Expr a) (Expr a))) (defn eval-int [e : (Expr int)] : int (match e (Lit n) n (If c t f) (eval-int t))) (eval-int (If (IsZero (Lit 0)) (Lit 7) (Lit 9))) ; => 7 ; ; doctest: a type declared inside the test body does not build when compiled
defgadt
(defgadt Name [a ...] (Ctor payload ... : Result) ...)
deprecated: a defdata whose every constructor declares its result type.
(defgadt Expr [a] (Lit int : (Expr int)) (IsZero (Expr int) : (Expr bool))) is defdata with one more rule: every constructor must carry its : ResultType (an unannotated one is requires an explicit return-type annotation). Everything else -- the head keywords, record constructors, what a refining constructor tells match -- is defdata's, which documents it. The form is deprecated (TUR-D0005, a warning; an error under --Werror=deprecated): change the keyword to defdata and leave the constructors as they are. tur explain TUR-D0005 shows the rewrite.
| Name | the type's name | |
| [a ..] -- the type parameters the constructors index | ||
| (Ctor payload ... : Result) -- constructors with their result types |
(defgadt Expr [a] (Lit int : (Expr int)) (Add (Expr int) (Expr int) : (Expr int)) (IsZero (Expr int) : (Expr bool))) (defn eval-int [e : (Expr int)] : int (match e (Lit n) n (Add l r) (+ (eval-int l) (eval-int r)))) (eval-int (Add (Lit 2) (Lit 40))) ; => 42 ; ; doctest: a type declared inside the test body does not build when compiled
defopaque
(defopaque Name base) (defopaque Name [A ...] base) (defopaque Name base :linear)
declare a newtype.
(defopaque Fd :int) makes Fd a type with exactly the representation of its base and no operations: it does not unify with int or with another opaque of the same base (expected Fd, got int; expected Fd, got Pid), and (+ (:: 1 Fd) 1) is a type error. Cross the boundary with ::, (:: n Fd) to wrap and (:: fd :int) to unwrap, which costs nothing. Use it for handles and branded ids. The base is :int, :ptr<void> or :ptr; :linear or :affine after it makes the value exactly-once or at-most-once, so (defopaque Tok :int :linear) must be consumed. A phantom type parameter goes before the base: (defopaque Tagged [A] :int) is written (Tagged int).
A float base works: (defopaque Celsius :float) is an int64_t handle holding the float's bits, and :: to or from it reinterprets them, so (:: (:: 21.5 Celsius) :float) is 21.5. An unknown base such as :string is an error.
| Name | the type's name | |
| [A ..] -- optional phantom type parameters | ||
| base | the representation: :int, :ptr<void> or :ptr | |
| marks | optional: :linear or :affine |
(defopaque Fd :int) (defn fd-num [fd : Fd] : int (:: fd :int)) (fd-num (:: 3 Fd)) ; => 3