Missing example of interaction with existential types?

[TD5]

This library is a really great example of pushing the limits of what you can do with F#!

When I created #26 and discussed this with someone, they quickly pointed out that GADTs are supposed to have something to do with existential types, but they couldn't actually see any existential types in the example! Below, I've captured what I think is going on. Does it make sense? Am I missing something?

The current example

I think the existing example is neat because it is so simple:

type 'a Expr =
| Const of Teq<int, 'a> * int
| Add of Teq<int, 'a> * Expr<int> * Expr<int>
| IsZero of Teq<bool, 'a> * Expr<int>
| If of Expr<bool> * Expr<'a> * Expr<'a>

In pseudocode (for readability and comparison to the literature):

Const  :: int                           -> Expr int
Add    :: Expr int -> Expr int          -> Expr int
IsZero :: Expr int                      -> Expr bool
If     :: Expr bool -> Expr a -> Expr a -> Expr a

However, I think it is actually too simple, and misses out on one of the key applications of GADTs!

A future example

Consider this example based on a snippet from wikipedia,

GADT definition pseudocode:

  Lift :: a                     -> Lam a        -- ^ lifted value
  Pair :: Lam a -> Lam b        -> Lam (a, b)   -- ^ product
  Lam  :: (Lam a -> Lam b)      -> Lam (a -> b) -- ^ lambda abstraction
  App  :: Lam (a -> b) -> Lam a -> Lam b        -- ^ function application

Evaluation function pseudocode:

eval (Lift v)   = v
eval (Pair l r) = (eval l, eval r)
eval (Lam f)    = \x -> eval (f (Lift x))
eval (App f x)  = (eval f) (eval x)

Notice how the App case is a bit special, because its a type parameter doesn't appear on the right-hand side of the constructor signature: App :: Lam (a -> b) -> Lam a -> Lam b. What this means is that when you have a Lam b in hand that happens to be in the App case, you don't know what the type of a is - you only know you have a Lam (a -> b) and a Lam a such that the a agrees (which means the type checker lets you apply one to the other)!

The implication here is that in order to construct this situation and hide the a away, you need a way to encode existentials! A while ago, I wrote about existentials in F#, but it would be really nice if there was a second example in this project which demonstrated how to bring these two ideas together.

[TD5]

It looks like there's some prior art out there, but I can see why you might want to be a bit careful in exposing it to beginners, because the boilerplate is scary even for a very simple example.

[njlr]

I was curious about this so decided to give it a go.

I used a crate for all cases except Lift, since I needed a way to introduce the type-parameter b.

Here is the code. Happy to make a PR if it seems correct.

Thanks!

#r "nuget: TypeEquality"

open TypeEquality

(*

  Lift :: a                     -> Lam a        -- ^ lifted value
  Pair :: Lam a -> Lam b        -> Lam (a, b)   -- ^ product
  Lam  :: (Lam a -> Lam b)      -> Lam (a -> b) -- ^ lambda abstraction
  App  :: Lam (a -> b) -> Lam a -> Lam b        -- ^ function application

*)

type Lam<'a> =
  | Lift of 'a
  | Pair of LamPairCrate<'a>
  | Abstraction of LamAbstractionCrate<'a>
  | Application of LamApplicationCrate<'a>

and LamPairEvaluator<'a, 'ret> =
  abstract Eval<'i, 'j> : Lam<'i> * Lam<'j> * Teq<'i * 'j, 'a> -> 'ret

and LamPairCrate<'a> =
  abstract Apply<'ret> : LamPairEvaluator<'a, 'ret> -> 'ret

and LamAbstractionEvaluator<'a, 'ret> =
  abstract Eval<'i, 'j> : (Lam<'i> -> Lam<'j>) * Teq<'i -> 'j, 'a> -> 'ret

and LamAbstractionCrate<'a> =
  abstract Apply<'ret> : LamAbstractionEvaluator<'a, 'ret> -> 'ret

and LamApplicationEvaluator<'a, 'ret> =
  abstract Eval<'i, 'j> : Lam<'i -> 'j> * Lam<'i> * Teq<'j, 'a> -> 'ret

and LamApplicationCrate<'a> =
  abstract Apply<'ret> : LamApplicationEvaluator<'a, 'ret> -> 'ret


[<RequireQualifiedAccess>]
module Lam =

  let lift (a : 'a) : Lam<'a> =
    Lift a


  let pair (x : Lam<'a>) (y : Lam<'b>) : Lam<'a * 'b> =
    let teq = Teq.Cong.pair Teq.refl Teq.refl
    Pair
      {
        new LamPairCrate<'a * 'b> with
          member this.Apply<'ret>(e : LamPairEvaluator<'a * 'b, 'ret>) =
            e.Eval(x, y, teq)
      }


  let abstraction (f : Lam<'a> -> Lam<'b>) : Lam<'a -> 'b> =
    let teq = Teq.Cong.func Teq.refl Teq.refl
    Abstraction
      {
        new LamAbstractionCrate<'a -> 'b> with
          member this.Apply<'ret>(e : LamAbstractionEvaluator<'a -> 'b, 'ret>) =
            e.Eval(f, teq)
      }


  let application (f : Lam<'a -> 'b>) (x : Lam<'a>) : Lam<'b> =
    let teq = Teq.refl
    Application
      {
        new LamApplicationCrate<'b> with
          member this.Apply<'ret>(e : LamApplicationEvaluator<'b, 'ret>) =
            e.Eval(f, x, teq)
      }


  // eval (Lift v)   = v
  // eval (Pair l r) = (eval l, eval r)
  // eval (Lam f)    = \x -> eval (f (Lift x))
  // eval (App f x)  = (eval f) (eval x)

  let rec eval<'a> (x : Lam<'a>) : 'a =
    match x with
    | Lift a -> a

    | Pair crate ->
      crate.Apply
        {
          new LamPairEvaluator<'a, 'a> with
            member this.Eval<'i, 'j>(x : Lam<'i>, y : Lam<'j>, teq : Teq<'i * 'j, 'a>) : 'a =
              let i = eval x
              let j = eval y
              Teq.cast teq (i, j)
        }

    | Abstraction crate ->
      crate.Apply
        {
          new LamAbstractionEvaluator<'a, 'a> with
            member this.Eval<'i, 'j>(f : Lam<'i> -> Lam<'j>, teq : Teq<'i -> 'j, 'a>) : 'a =
              let g = fun i -> eval (f (lift i))
              Teq.cast teq g
        }

    | Application crate ->
      crate.Apply
        {
          new LamApplicationEvaluator<'a, 'a> with
            member this.Eval<'i, 'j>(f : Lam<'i -> 'j>, x : Lam<'i>, teq : Teq<'j, 'a>) : 'a =
              let j = eval f (eval x)
              Teq.cast teq j
        }




// Tests

#r "nuget: Expecto"

open Expecto

let tests = testList "Lam.eval" [
  test "Lam.lift" {
    let x = Lam.lift 123

    Expect.equal (Lam.eval x) 123 ""
  }

  test "Lam.pair" {
    let x = Lam.pair (Lam.lift "abc") (Lam.lift true)

    Expect.equal (Lam.eval x) ("abc", true) ""
  }

  test "Lam.application 1" {
    let addOne = Lam.abstraction (fun x -> Lam.lift (Lam.eval x + 1))
    let x = Lam.application addOne (Lam.lift 123)

    Expect.equal (Lam.eval x) 124 ""
  }

  test "Lam.application 2" {
    let adder =
      Lam.abstraction (fun x ->
        Lam.abstraction (fun y -> Lam.lift (Lam.eval x + Lam.eval y)))

    let add x y =
      Lam.application (Lam.application adder x) y

    let x = add (Lam.lift 3) (Lam.lift 4)

    Expect.equal (Lam.eval x) 7 ""
  }
]

runTestsWithCLIArgs [||] [| "--summary" |] tests

[Smaug123]

Yes, that looks about right to me! I'm happy to let you PR that if you particularly want to, or for me to do it. (Note that we use NUnit rather than Expecto. Personally I'd also implement Fix because the Wikipedia page does, and I'd put quite a lot of documentation in because simply-typed lambda calculus isn't very familiar to many people.)