tur/forms/types

(as type expr)

convert a number to another numeric kind.

The first argument is a bare numeric type name, not evaluated: int, int8 ... int64, uint8 ... uint64, float, float32, float64 (a keyword such as :int8 is 'as' expects a type name as first argument, and a non-numeric target such as bool is 'as' casts are only valid for numeric types). Arithmetic does not mix widths implicitly, so (+ 1i8 (as int8 2i16)) is how a narrower or wider operand is brought to match.

Integer to integer keeps the low bits: (as int8 300) is 44 and (as uint8 -1) is 255. Integer to float is the nearest float, and a float to an integer discards the fraction toward zero: (as int 7.9) is 7 and (as int -7.9) is -7. A float outside the range of the integer it is converted to has no defined answer, and the two engines differ: (as uint8 300.7) is 255 compiled (it saturates) and 44 interpreted. Keep the value in range first.

(as int 7.9)  ; => 7
(as uint8 -1)  ; => 255
(as float32 7.1)  ; => 7.1

(:: expr type)

give a value another type without converting it.

(:: expr Type) is a type ascription. The type is a keyword or a bare name (:int, int, Meters, (Option float), ptr<void>, any). It moves a value across a boundary the checker would otherwise stop at, and never changes the bits: (:: n Meters) makes an int into a defopaque newtype and (:: m :int) takes it back; (:: true :int) is 1 and (:: 1 :bool) is true; an integer literal given a float type becomes that float ((:: 3 :float) is 3.0). Nothing is wrapped or rounded -- (:: 300 :int8) is still 300; use as for a conversion.

An ascription between an integer kind and a float kind is a compile error because it could mean convert or reinterpret: use float->int / int->float (stdlib/math.tur) to convert and float->bits (stdlib/bits.tur) to read the bits. An aggregate passed by value (a :copy struct) cannot be ascribed to :int or ptr<void> (TUR-E0295): box it into any. An any cannot be ascribed back to a type -- :: asserts a representation and an any is a tagged pair -- so use cast, which checks the tag. Ascribing a string to :int yields its address compiled and leaves the string interpreted; do not rely on either.

(:: true :int)  ; => 1
(:: 1 :bool)  ; => true
(:: 7.1 :float32)  ; => 7.1

(? expr)

return early from a function when a Result (or Option) is an error.

(? expr), or ?(expr) in neoteric syntax, evaluates expr once. If it is an error the enclosing function returns it; otherwise the ? is the ok value. It is written inside a function body (? operator is only allowed inside a function body) and the function must itself return the same kind of value. A non-Result operand such as (? 5) is TUR-E0001.

An operand statically typed (Result T E) -- a variable, or a call of a named function that returns one -- lowers to (if (err? q) (return (Err (err-val q))) (ok-val q)), so the error type must agree and the ok type may differ; a (Option T) operand lowers the same way with None and unwrap. That works on every engine. Any other operand (a call whose result type is not known without elaborating it, or a Result carried as a ptr<void>) takes the older route through the __tur-q-is-err? / __tur-q-ok-val helpers in stdlib/result.tur, which read the pointer layout and do not run interpreted; bind such a value to a typed variable first.

(defn halve [n : int] : (Result int cstr) (if (= (mod n 2) 0) (ok (/ n 2)) (err "odd")))
(defn quarter [n : int] : (Result int cstr) (let [h (? (halve n))] (halve h)))

(cast x type)

take a value out of an any, checking its type.

An any carries a value and a tag naming its type. (cast x Type) reads the value back as Type if the tag matches, and panics otherwise (cast: any holds float, not int). x must be an any; a plain value is 'cast' expects an 'any'-typed first argument, and an unknown Type is unknown type 'Nope' in 'cast'. A parametrised type is written applied, (cast x (Option int)); the bare constructor Option is an error. Test first with is? to avoid the panic.

(cast (:: 7.1 any) float)  ; => 7.1
(cast (:: "hi" any) cstr)  ; => "hi"

(is? x type)

test what type an any is carrying.

(is? x Type) is true when the any x was made from a value of type Type. x must be an any ('is?' expects an 'any'-typed first argument otherwise). A parametrised type is written applied: (is? x (Option int)) is true for (:: (Some 3) any) and (is? x (Option float)) is false compiled, while the interpreter, which does not record the instantiation, says true for both. Sized numbers differ the same way: (is? (:: 3i32 any) int32) is true compiled and false interpreted.

(is? (:: 7.1 any) float)  ; => true
(is? (:: 42 any) float)  ; => false

(type-of [x :any] :cstr)

the name of the type an any is carrying.

Takes an any and returns the type's name as a string: float, int, cstr, bool, Sym for a keyword, fn for a function, the type name of a struct or ADT (Option without its instantiation). A value that is not already an any is 'type-of' expects an 'any'-typed argument. A sized integer is named for its size when compiled (int32 for (:: 3i32 any), uint8, ...); the interpreter has one integer and one float kind and says int / float. A float32 is widened as a float, so it reads float on both. See is?.

(type-of (:: 7.1 any))  ; => "float"
(type-of (:: "hi" any))  ; => "cstr"

(coerce proof x)

use an Equal proof to treat a value as another type.

(coerce proof x) evaluates proof, which must be a value of the Equal type ((Refl) after (load "stdlib/equal.tur"), or a parameter annotated with the bare name Equal or applied, (Equal int int)), and returns x. Nothing is converted and no code is emitted. With proof : (Equal a b) and x : a, the result has type b: (defn conv [A B] [eq : (Equal A B) x : A] : B (coerce eq x)) type-checks, and (conv (Refl) 7.1) is a float -- the call reads B = A from Refl's (Equal a a). With the bare Equal annotation the result keeps x's own type. An applied proof checks that its a is x's type when both are concrete (coerce: the proof is about a value of type ...), and a proof relating two different concrete types, (Equal int float), is coerce: the proof (Equal int float) relates different types -- Refl cannot be built there. A proof (Equal A int) with a type-variable a and a concrete b still returns x at A. A session channel cannot be coerced. A first argument that is not an Equal is coerce requires an (Equal a b) proof.

(load "stdlib/equal.tur")
(println (coerce (Refl) 42))  ; prints 42
(defn conv [A B] [eq : (Equal A B) x : A] : B (coerce eq x))
(println (conv (Refl) 7.1))   ; prints 7.1

(type-app F A)

removed: write the applied type (F A).

(type-app F A) used to be the explicit spelling of applying the type constructor F to the type A. In a type annotation it never worked (it was TUR-E0012 cannot apply a type of kind '*' as a type constructor for every constructor), and as a statement it checked an arity and did nothing. It is now an error in every position that names the spelling to use instead: (type-app Option int) is type-app has been removed: write the applied type (Option int). The word stays reserved for a release. Messages print a type application the same way, (Option float).

(defn size [o : (Option int)] : int 0)  ; not (type-app Option int)

(forall [a ...] type)

a type that works for every type: polymorphic arguments.

Appears in a type, never as an expression. In a parameter annotation, [f (forall [a] (-> a a)) x : int], it makes f a rank-2 function: the callee may use f at any type it likes, so (f x) with an int and (f s) with a cstr in the same body both type-check, and the caller must pass a function that is generic in that way (hrt-guide). Several variables go in the bracket, (forall [a b] (-> a b a)), and a typeclass constraint after them, (forall [a] [(Show a)] (-> a cstr)); a bound variable can carry a kind, (forall [(f :: * -> *)] ...). The argument must be a named function or a lambda that captures nothing (a capturing one is rank-2 argument must be a named function); a non-function is expected ptr<void>, got int; and a poly function cannot be stored in a list or option.

The function passed must be generic wherever the forall body has a bare bound variable: its parameter there is a type parameter ([A] [x : A]) or un-annotated -- not any, a tagged value the untyped word cannot fill (TUR-E0001 says so). Passing inc : int -> int where (forall [a] (-> a a)) is expected is rank-2 argument 'inc' is not generic (TUR-E0001), for a named function, a lambda, or a function defined later in the file alike. When the callee only ever applies it at the type it handles, ascribe it to the forall type to say so: (apply-poly (:: inc (forall [a] (-> a a))) 7). The ascription is trusted, not checked. Not checked yet: the result type, and a variable under a type application such as (List a).

(defn id [x] x)
(defn apply-poly [f (forall [a] (-> a a)) x : int] : int (f x))
(println (apply-poly id 7))  ; prints 7

(exists [a ...] type)

a type whose concrete part is hidden.

Appears in a type. (exists [a] T) is a value of some type a that the holder cannot name, packaged with whatever T says about it, and (exists [a] [(Show a)] a) adds the typeclass operations the holder may use on it. It is the dual of forall: there the caller chooses the type, here the maker does. Values are made with pack and used with open; a function can take one, [e : (exists [a] [(Show a)] a)], or return one. Values of different types that share the class can then be handled alike (existential-types-guide).

(pack value type)

hide a value's type inside an existential.

(pack value (exists [a] [(C a)] a)) makes the existential. At the pack site the compiler checks that the value's type has an instance for each constraint (pack: no instance 'Shape' for type 'int' otherwise); the result carries the value and the evidence for the constraints, so values of different types can be treated alike afterwards. Without constraints, (pack 42 (exists [a] a)), nothing can be done with the value but hide it. The (pack int 0) spelling in hrt-guide is not accepted.

(defclass Show [a] (show [x] : cstr))
(definstance Show [int] (show [x] : cstr "an int"))
(defn main [] : int
  (let [e (pack 42 (exists [a] [(Show a)] a))]
    (open e [_ v] (println (show v))))  ; prints an int
  0)

(open e [a v] body)

use the value inside an existential.

(open e [a v] body) unpacks the existential e: inside body, v is the hidden value, a is its type as an abstract name that matches only itself, and the class operations promised by the type work on v: (show v) or (.show v). The binder for the type can be _. The result of body may not mention a, so the value cannot leave: returning v itself is open: existential type variable 'a' escapes its scope. The unpacking uses the evidence packed with the value to choose the operation, so two packed values of different types each reach their own instance -- two defopaque types over :int included, on every engine.

(open (pack 42 (exists [a] a)) [a v] 7)  ; => 7

(& place)

borrow a value without taking it.

(& place), written &place, makes an immutable borrow of type &T: a reference to a variable, a field (&(.x p)) or another borrow (a reborrow is still &T). Read through it with @r; a borrow is not itself a number, so (println r) is a type error and (println @r) prints the value. Any number of immutable borrows of one variable may exist together. A parameter is typed r : &int. The checker rejects a function that returns a borrow of its own local (TUR-E0105). A borrow lasts to the end of the enclosing let, so borrowing x mutably afterwards in that same let is cannot borrow 'x' as mutable while it is already borrowed; close the let first.

While a let holds a borrow of a place, set! of that place is refused if the borrow is used after the assignment (cannot assign to 'x' while it is borrowed by 'r'); a borrow the body is done with does not block the write. A borrow of a literal ((& 7.25)) borrows a temporary that lives as long as the let holding it.

(let [x 41] (let [r &x] @r))  ; => 41

(&mut place)

borrow a value so it can be changed through the borrow.

(&mut place), written &mut place, makes an exclusive borrow of type &mut T. Write through it with (set! @r value); reading is @r. While it lives no other borrow of the same variable may be made, mutable or not (cannot borrow 'x' as immutable while it is mutably borrowed), and the variable itself is not changed behind its back. A parameter is typed r : &mut int, so a helper can change its caller's variable: (defn bump [r : &mut int] : nil (set! @r (+ @r 1))) called as (bump &mut x).

The place must be one set! could write: a ^mut variable or a field of one (cannot borrow 'x' as mutable: it is not declared '^mut'). A place behind an rc, a :heap struct or another borrow needs nothing.

(let [^mut y 5] (let [m &mut y] (set! @m 42)) y)  ; => 42