Reference

;; First form. Implicitly typed variable definition.
;;
;; Bind the global variable ~fst-iv~ to the function that
;; extracts the first value of a pair. No explicit type
;; signature is given - it is statically inferred by the
;; typechecker to be the equivalent of ~(forall (a b) (Fun
;; (Pair a b) a))~
(define fst-iv
  (fun ((Pair x _)) x))

;; Second form. Implicitly typed function definition.
;;
;; Again, the fst function, equivalent to the defition
;; above, but using the more convenient function definition
;; syntax.
(define (fst-if p)
  (match p
    (case (Pair x _) x)))
;; ... and again, together with the even more conventient
;; destructuring syntax
(define (fst-ifd (Pair x _))
  x)

;; Third form. Explicitly typed variable definition.
;;
;; Explicit type signature is given. The type must properly
;; be a polytype (aka /type scheme/) to be valid and
;; instantiable for any monotype.
(define: fst-ev
    (forall (a b) (Fun (Pair a b) a))
  (fun-match (case (Pair x _) x)))

;; Fourth form. Explicitly typed function definition.
(define: (fst-ef (Pair x _))
    (forall (a b) (Fun (Pair a b) a))
  x)

;; First form. Monomorphic datatype definition.
;;
;; ~Age~ only has one variant, and as such can be seen as a
;; "wrapper" around ~Int~, restricting its usage.
(type Age
  (Age Int))

;; Second form. Polymorphic datatype definition.
;;
;; ~List~ has two variants, representing that a list can
;; either be empty, or a pair of a head and a tail. Note
;; that we must have a ~Box~ indirection so that it doesn't
;; have infinite size.
(type (List' a)
  (Cons' a (Box (List' a)))
  Nil')

;; An uninhabited type that can't be constructed. Useful
;; when you want to employ the type system to make invalid
;; states unrepresentable, or model propositions as types.
(type Void')

(define (id-int x)
  (: x Int))
;; Inferred type of ~id-int~: (Fun Int Int)

(type Foo
  Bar
  Baz)
(type (Pair' a b)
  (Pair' a b))

;; Ok
(define (fst' pair)
  (match pair
    (case (Pair' a _) a)))

;; Matching on an uninhabited type corresponds to the
;; elimination rule for ⊥ (it implies anything).
(define: (absurd void)
    (forall (a) (Fun Void' a))
  (match void))

(define read-binop
  (fun-match
    (case "plus" +)
    (case "times" *)
    (case s (panic (str-append "Undefined binop " s)))))

;; Error. Redundant pattern. ~Pair _ _~ already covered by
;; previous pattern ~_~
(define (redundant pair)
  (match pair
    (case _ 1)
    (case (Pair' x y) 2)))

;; Error. Inexhaustive pattern. All cases not covered,
;; specifically ~Bar~
(define (inexhaustive foo)
  (match foo
    (case Baz 123)))

;; Two versions of `fst`, which returns the first value of a
;; pair
;;
;; using normal `match`
(define (fst-nofun p)
  (match p
    (case (Pair a _) a)))
;; and using `fun-match`
(define fst-fun
  (fun-match
    (case (Pair a _) a)))

;; The following datatype definition will make available the
;; constructors ~UPUnit~ and ~UPPair~ in the environment.
(type UnitOrPair
  UPUnit
  (UPPair Int Int))


;; The ~UPUnit~ constructor is nullary, and will construct a
;; ~UnitOrPair~ just presented literally.
(define: upunit
    UnitOrPair
  UPUnit)

;; The ~UPPair~ constructor is binary, and takes two
;; arguments to construct a ~UnitOrPair~. It behaves like a
;; function of two ~Int~ arguments, returning a
;; ~UnitOrPair~.
(define: uppair''
    (Fun Int Int UnitOrPair)
  UPPair)
(define: uppair'
    (Fun Int UnitOrPair)
  (UPPair 3))
(define: uppair
    UnitOrPair
  (uppair' 5))