Row types?

Stream: Is there code for X?

[aron]

I'm trying to see if I can implement something like row types. Like a record whose fields can be manipulated, and where you can specify that a function takes a record that has at least fields x : Int and y : ?any and it will accept any arbitrary record type as long as it has those two fields.

I'm trying to do this with a subtype of Std.HashMap that contains Strings as keys and whose key labels and value types are listed in the type index, but finding it quite difficult to do this. Has someone tried doing something like this before?

[Aaron Liu]

What is ?any?

[aron]

Oh just a placeholder for any type. My point being that unlike for the field x which must have the specific type Int, I don't care what type the field yhas, just that the record has such a field

[aron]

This becomes more useful if you think of a function like { r | y : a } -> a

That's the Elm notation for row types. In that example the r represents the full record type, and the a is a type variable that unifies with whatever type the y field in its input value has

[Aaron Liu]

Are you sure you want any type?

[Aaron Liu]

Std.HashMap Int (Sigma fun t : Type => t) map integers to arbitrary types.

[Aaron Liu]

But since you are now effectively quantifying over all Types this ends up being a Type 1.

[aron]

ok so let's just worry about concrete types for now

[aron]

like how would you encode a row type that has x : Int and y : String fields but which can be extended with more fields

[Aaron Liu]

If it's extended then it's not the same type anymore?

[Aaron Liu]

We have structure types

[Aaron Liu]

structure Foo where
  x : Int
  y : String

def Foo.getInt (f : Foo) : Int := f.x

structure Bar extends Foo where
  z : Float

def foo : Foo where
  x := 0
  y := ""

def bar : Bar := {foo with z := 37}

-- 0
#eval foo.getInt
-- 0
#eval bar.getInt

[Eric Wieser]

You could use typeclasses to achieve this:

import Mathlib

class HasField (α : Type*) (name : Lean.Name) (β : outParam <| α → Type*) where
  field (a : α) : β a

structure IncludesX where
  x : Int
  y : Int

instance : HasField IncludesX `x (fun i => type_of% i.x) where
  field i := i.x

-- optional custom notation
syntax term noWs ".!" ident : term
macro_rules
| `($t:term.!$n:ident) => `(HasField.field $(Lean.quote n.getId) $t)

def actWithX [HasField α `x (fun _ => Int)] (a : α) := a.!x

def foo : IncludesX := ⟨2, 3⟩

#eval actWithX foo

[aron]

@Aaron Liu ah interesting, I don't think I knew you could extend structure types like that.

But if I'm not mistaken, you still can't have a lean function that takes any structure type containing a particular field, can you? To say that my function f takes any structure containing a field x : Int and have it accept both Foos and Bars alike?

E.g. this doesn't work:

def getX (v : Foo) : Int := v.x

def myX := getX {x := 0, y := ".", z := 0.1}

Whereas row polymorphism would let you do something like:

def getX {m} (v : { m | x : Int}) : Int := v.x

def myX := getX {x := 0, y := ".", z := 0.1}

[Eric Wieser]

My [HasField α `x (fun _ => Int)] above does exactly that

[aron]

@Eric Wieser ooh interesting... :eyes: I really like the .!x notation you've implemented!

If I'm understanding your code correctly this requires you to implement a separate instance of HasField for every permutation of field name × field type you might want to use?

Is there a way to automatically infer the return type at least so you only have to make a new instance per field name, not per name × type? I don't understand exactly how outParam works, but is it not possible to use it to make the return type be inferred from the getter function you use for β in each instance?

I'm trying this but it doesn't work:

import Mathlib

class HasField (α : Type*) (name : Lean.Name) (β : outParam <| α → Type*) where
  field (a : α) : β a

structure IncludesX {t : Type*} where
  x : Int
  y : Int
  z : t

instance {t} : HasField (@IncludesX t) `x (fun _ => t) where
  field i := i.x
--           ^^^

[aron]

Also, with your implementation you still have to manually make sure that the Name you want to use in the .!<name> notation matches the field name of the underlying structure you want to make a getter for, right?

[Eric Wieser]

No, you can't avoid needing an instance for every (type, field) pair

[Eric Wieser]

But you can generate them automatically with a metaprogram

[Eric Wieser]

Edited above to use type_of% to make it a little clearer how to write such a program

[aron]

oh that's really nice! mm ok I need to look more into metaprogramming in lean because if there are more of these little things that can make my code simpler and more general I want to know about them