Newtypes: phantom type parameters

One Id with a tag for what it is an id of, in place of a newtype per kind
of id, and a tag that records what has been checked about a value, kept
honest by #:opaque.

🤖 Generated with [ECA](https://eca.dev)

Co-Authored-By: eca-agent <git@eca.dev>

_01.Language-basics.sz

@@ -375,6 +375,44 @@ A newtype is the opposite of an alias: a type of its own, which the compiler wil
 
 A newtype does not get the traits of the type it wraps: @code{(+ u u)} is an error, though @code{(+ 7 7)} is not. It gets those you give it, as the section on traits shows.
 
+A newtype can have a type parameter that its value does not use. Such a parameter is called a @em{phantom}: it is only there to tell values apart. Instead of one newtype for each kind of id, there can be one @code{Id} that says what it is an id of. The tags are types with no values, written as unions with no cases:
+
+@codeblock[#:lang "bjolang"]|{
+(type (: User (Union)))                ;; tags: types with no values
+(type (: Order (Union)))
+(type (: (Id %a) (Newtype int)))       ;; %a is in no field
+
+(: lookup-user (-> (Id User) string))
+(defun (lookup-user id) ...)
+
+(: id-number (-> (Id %a) int))         ;; for an id of any kind
+(defun (id-number id)
+  (def (Id n) id)
+  n)
+
+(lookup-user (: (Id 7) (Id Order)))    ;; a compile error: an (Id Order) is not an (Id User)
+}|
+
+An @code{(Id User)} is still an @code{int} when the program runs. A function can be written once for every kind of id, as @code{id-number} is, and a trait can have an implementation for each tag, such as one for @code{(Id User)} and another for @code{(Id Order)}.
+
+A tag can also record what has been checked about a value. Here only @code{validate} can make an @code{(Email Valid)}, so @code{send} never gets an address nobody checked:
+
+@codeblock[#:lang "bjolang"]|{
+(type (: Raw (Union)))
+(type (: Valid (Union)))
+(type (: (Email %s) #:opaque (Newtype string)))
+
+(: validate (-> (Email Raw) (Option (Email Valid))))
+(defun (validate e)
+  (def (Email s) e)
+  (if (string-contains? s "@") (Some (Email s)) None))
+
+(: send (-> (Email Valid) void))
+(defun (send e) ...)
+}|
+
+@code{#:opaque}, described under exporting types in "Writing programs", is what keeps another module from building an @code{(Email Valid)} itself, with @code{(Email s)}.
+
 @subsubsection{Records and structs}
 Records and structs are direct mappings to c# records and immutable structs. The constructor is the type name, together with parenthesised fields. As follows.