Ship

Book · Indexed variants

Indexed variants

Draft

Closed variants whose cases fix their type's parameters, refined by matching.

On this page · 4 sections

A case may declare the type its constructor builds. IntLit builds only an Expr(Int) and Equal only an Expr(Bool), so the parameter of Expr records what each expression evaluates to. Type variables written in a case belong to that constructor alone. These are generalized algebraic data types (GADTs).

type Expr('value) =
  | IntLit(Int): Expr(Int)
  | BoolLit(Bool): Expr(Bool)
  | Add(Expr(Int), Expr(Int)): Expr(Int)
  | Equal(Expr(Int), Expr(Int)): Expr(Bool)
  | If(Expr(Bool), Expr('value), Expr('value)): Expr('value)
  | Pair(Expr('left), Expr('right)): Expr(('left, 'right))

Matching refines

Matching a case teaches its arm what the case fixed. Inside IntLit(value) the arm knows 'value is Int, so it returns value where the signature promises 'value. Refinement happens only against type variables a written signature holds rigid, which is why eval states its type.

let rec evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr('value)) -> 'value, exn [ 'b ], eff 'c = fn('value)(exprexpr: Book.LanguageReference.IndexedVariants.Expr('a): Expr('value)) -> 'value {
  match exprexpr: Book.LanguageReference.IndexedVariants.Expr('a) {
    | IntLit(valuevalue: Int) -> valuevalue: Int
    | BoolLit(valuevalue: Bool) -> valuevalue: Bool
    | Add(leftleft: Book.LanguageReference.IndexedVariants.Expr(Int), rightright: Book.LanguageReference.IndexedVariants.Expr(Int)) -> evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Int)) -> Int, exn [ 'a ], eff 'b(leftleft: Book.LanguageReference.IndexedVariants.Expr(Int)) + evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Int)) -> Int, exn [ 'a ], eff 'b(rightright: Book.LanguageReference.IndexedVariants.Expr(Int))
    | Equal(leftleft: Book.LanguageReference.IndexedVariants.Expr(Int), rightright: Book.LanguageReference.IndexedVariants.Expr(Int)) -> evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Int)) -> Int, exn [ 'a ], eff 'b(leftleft: Book.LanguageReference.IndexedVariants.Expr(Int)) == evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Int)) -> Int, exn [ 'a ], eff 'b(rightright: Book.LanguageReference.IndexedVariants.Expr(Int))
    | If(conditioncondition: Book.LanguageReference.IndexedVariants.Expr(Bool), yesyes: Book.LanguageReference.IndexedVariants.Expr('a), nono: Book.LanguageReference.IndexedVariants.Expr('a)) -> if evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Bool)) -> Bool, exn [ 'a ], eff 'b(conditioncondition: Book.LanguageReference.IndexedVariants.Expr(Bool)) {
      | evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr('value)) -> 'value, exn [ 'b ], eff 'c(yesyes: Book.LanguageReference.IndexedVariants.Expr('a))
      | evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr('value)) -> 'value, exn [ 'b ], eff 'c(nono: Book.LanguageReference.IndexedVariants.Expr('a))
    }
    | Pair(leftleft: Book.LanguageReference.IndexedVariants.Expr('a), rightright: Book.LanguageReference.IndexedVariants.Expr('a)) -> (evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr('value)) -> 'value, exn [ 'b ], eff 'c(leftleft: Book.LanguageReference.IndexedVariants.Expr('a)), evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr('value)) -> 'value, exn [ 'b ], eff 'c(rightright: Book.LanguageReference.IndexedVariants.Expr('a)))
  }
};

Evaluate

test✓
  expect ✓evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Int)) -> Int, exn [ 'a ], eff 'b(Add(IntLit(11: Int), IntLit(22: Int))) == 33: Int;
  expect ✓evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Bool)) -> Bool, exn [ 'a ], eff 'b(Equal(IntLit(22: Int), Add(IntLit(11: Int), IntLit(11: Int))));
  expect ✓evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr(Int)) -> Int, exn [ 'a ], eff 'b(If(BoolLit(FalseFalse: Bool), IntLit(11: Int), IntLit(22: Int))) == 22: Int;
  expect ✓evaleval: fn('value)(expr: Book.LanguageReference.IndexedVariants.Expr((Int, Bool))) -> (Int, Bool), exn [ 'a ], eff 'b(Pair(IntLit(11: Int), BoolLit(TrueTrue: Bool))) == (11: Int, TrueTrue: Bool);

Impossible cases

Coverage skips a case whose declared result can never be the matched type. An Expr(Bool) is never an IntLit, an Add, or a Pair, so a match on one lists only the cases that can build it.

let describedescribe: fn(expr: Book.LanguageReference.IndexedVariants.Expr(Bool)) -> String = (exprexpr: Book.LanguageReference.IndexedVariants.Expr(Bool): Expr(Bool)) -> String =>
  match exprexpr: Book.LanguageReference.IndexedVariants.Expr(Bool) {
    | BoolLit(_) -> "literal""literal": String
    | Equal(_, _) -> "comparison""comparison": String
    | If(_, _, _) -> "choice""choice": String
  };

Impossible Cases

test✓
  expect ✓describedescribe: fn(expr: Book.LanguageReference.IndexedVariants.Expr(Bool)) -> String(Equal(IntLit(11: Int), IntLit(11: Int))) == "comparison""comparison": String;
  expect ✓describedescribe: fn(expr: Book.LanguageReference.IndexedVariants.Expr(Bool)) -> String(If(BoolLit(TrueTrue: Bool), BoolLit(FalseFalse: Bool), BoolLit(TrueTrue: Bool))) == "choice""choice": String;

Existential payloads

A variable that appears only in a case's payload is chosen by whoever builds the value and stays abstract to whoever matches it. Shown packs a value with the one function that can use it; the arm may apply show to value, but the value's type cannot leave the arm.

type Shown =
  | Shown('value, fn(value: 'value) -> String): Shown

let renderrender: fn(shown: Book.LanguageReference.IndexedVariants.Shown) -> String = (shownshown: Book.LanguageReference.IndexedVariants.Shown: Shown) -> String =>
  match shownshown: Book.LanguageReference.IndexedVariants.Shown {
    | Shown(valuevalue: 'a, showshow: fn(value: 'a) -> String) -> showshow: fn(value: 'a) -> String(valuevalue: 'a)
  };

Existential Payloads

test✓
  expect ✓renderrender: fn(shown: Book.LanguageReference.IndexedVariants.Shown) -> String(Shown(33: Int, (valuevalue: Int: Int) => Int.to_stringto_string: pure fn!(value: Int) -> String(valuevalue: Int))) == "3""3": String;
  expect ✓renderrender: fn(shown: Book.LanguageReference.IndexedVariants.Shown) -> String(Shown("ready""ready": String, (valuevalue: String: String) => valuevalue: String)) == "ready""ready": String;

Behaviors

An indexed variant synthesizes no behaviors. Each case fixes the type's parameters differently, so no one generic implementation serves every case, and decoding could not know which case's type it builds. Write the modules a program needs.

Rejected programs lists the declarations and matches Ship refuses.