Purescript-style Variants (dual of records)?

Stream: Is there code for X?

[André Muricy Santos]

Purescript has the notion of variants, which are basically the dual of row-type based anonymous records. If records allow for things like

modify :: forall r. { field :: Int | r } -> { field :: String | r }
modify x = let newVal = show (add 10 x.field) in x { field = newVal }

then variants allow for things like:

allToString :: forall r. Variant (foo :: Int, bar :: Boolean | r ) -> String
allToString =
  default "unknown"
    # on (Proxy :: Proxy "foo") show
    # on (Proxy :: Proxy "bar") (\x -> if x then "true" else "false")

This is all thanks to the fact that the compiler has efficient ordered rows, which are basically type-level lists of string (name of field) and type (type of field) tuples.

Since Lean has dependent types I'm sure it has sufficient expressive power for both variants and anonymous records, and with metaprogramming even some convenient syntax could be built?

[Kyle Miller]

Here's a typeclass-based experiment with row types, though it doesn't handle reordering rows. Something similar should be possible for variants and ⊕.

import Lean

open Lean

def WithField (name : Name) (α : Type _) (r : Type _) := α × r

macro "field(" name:ident " : " α:term ")" " × " r:term : term =>
  `(WithField $(quote name.getId) $α $r)

class GetField (name : Name) (ty : Type _) (α : outParam <| Type _) where
  proj : ty → α

instance (priority := low) [GetField name r α] : GetField name (WithField name' α' r) α where
  proj x := GetField.proj name x.2

instance : GetField name (WithField name α r) α where
  proj x := x.1

class SetField (name : Name) (ty : Type _) (α : Type _) (ty' : outParam <| Type _) where
  set : ty → α → ty'

instance (priority := low) [SetField name r α r'] :
    SetField name (WithField name' α' r) α (WithField name' α' r') where
  set x v := (x.1, SetField.set name x.2 v)

instance : SetField name (WithField name α r) α' (WithField name α' r) where
  set x v := (v, x.2)

def modify1 {r} (x : field(f : Int) × r) : field(f : String) × r :=
  let newVal := 10 + GetField.proj `f x
  SetField.set `f x (toString newVal)

def modify2 {r} (x : field(fst : String) × field(snd : String) × r) :
    field(fst : String) × field(snd : String) × r :=
  SetField.set `fst (SetField.set `snd x (GetField.proj `fst x)) (GetField.proj `snd x)

#eval modify1 (22, "a", ())
-- ("32", "a", ())

#eval modify2 ("a", "b", ())
-- ("b", "a", ())