RFC: Anonymous records and polymorphic field constrants

Stream: lean4

[Serhii Khoma (srghma)]

Summary

purescript has Anonymous records and polymorphic field constrants

https://github.com/purescript/documentation/blob/master/language/Records.md

https://pursuit.purescript.org/builtins/docs/Prim#t:Row
https://pursuit.purescript.org/builtins/docs/Prim.Row
https://pursuit.purescript.org/builtins/docs/Prim.RowList

Motivation

1. Why anonymous records are great?

they are shorter

data Foo
  = Foo1 { hehe :: String, hoho :: String }
  | Foo2 { hehe :: Int, hoho :: Int }

2. Why polymorphic field constrants is great?

rn can implement

-- A function that works on any record with a name field
sayHello : { r | name : String } -> String
sayHello person = "Hello, " ++ person.name ++ "!"

-- Compatible with multiple records
greeting1 : String
greeting1 = sayHello { name = "Alice", age = 25 }

greeting2 : String
greeting2 = sayHello { name = "Charlie", city = "London" }

what You think, guys, if I would implement it for lean4? how it would look like?

P.S.

(from idris2 discord channel): idris2 has https://github.com/kuribas/idris-records and it allows to implement polymorphic field constrants

sayHello : HasField "name" String s => SimpleRecord s -> String
sayHello r = "Hello " ++ (r !! "name") ++ "!"

but not

data Foo
  = Foo1 { hehe :: String, hoho :: String }
  | Foo2 { hehe :: Int, hoho :: Int }

P.S. we need channel exlusively for prs for lean4

[Patrick Massot]

If you really don't want more than what you showed in your example then you can use a macro.

[Eric Wieser]

I don't really see any great benefit to HasField "name" String vs clas MyHasName A where name (a : A) : String

[Eric Wieser]

serhii khoma (srghma) said:

data Foo
  = Foo1 { hehe :: String, hoho :: String }
  | Foo2 { hehe :: Int, hoho :: Int }

Can you elaborate on what is different here vs what Lean already has?

inductive Foo
  | Foo1 ( hehe : String) (hoho : String)
  | Foo2 { hehe : Int) (hoho : Int)

[Serhii Khoma (srghma)]

Eric Wieser said:

Can you elaborate on what is different here vs what Lean already has?

inductive Foo
  | Foo1 ( hehe : String) (hoho : String)
  | Foo2 { hehe : Int) (hoho : Int)

positional arguments very easily allow to miss order of arguments

inductive Foo
  | Foo1 (hehe : String) (hoho : String)
  | Foo2 (hehe : Int) (hoho : Int)

def x : Foo := Foo.Foo1 "hoho" "hehe"

while with records this is would be impossible

inductive Foo
  | Foo1 { hehe : String, hoho : String }
  | Foo2 { hehe : Int, hoho : Int }

def x : Foo := Foo.Foo1 { hehe: "hehe", hoho: "hoho" }

-- and order is arbitrary
def y : Foo := Foo.Foo1 { hoho: "hoho", hehe: "hehe" }

[Serhii Khoma (srghma)]

Patrick Massot said:

If you really don't want more

like what for example?

than what you showed in your example then you can use a macro.

could You demonstrate? tnx

[Kyle Miller]

Are you familiar with named arguments?

def x : Foo := Foo.Foo1 (hoho := "hoho") (hehe := "hehe")

[Serhii Khoma (srghma)]

Kyle Miller

but how about using multi-valued records in already existing types

How to write something like this in lean?

NOTE: in purescript it generates the Eq type automatically

import Data.Either

type MyError = Either { name :: String, message :: String } { foo :: Int, bar :: Int }

isEq :: Boolean
isEq = (Left { name: "1", message: "message" } :: MyError) == Left { name: "2", message: "message" }

like https://github.com/kuribas/idris-records/blob/4a5784648d3f8b544e7a375431fa70698e8ed6fc/src/Records.idr#L47 but with macros

---

and supporting it in lean would allow to generate efficient code (e.g. if in future lean will be able to generate javascript - then use ordinary javascript Object)

[Daniel Weber]

You can do this in Lean using deriving

import Lean

inductive Foo
  | Foo1 (hehe : String) (hoho : String)
  | Foo2 (hehe : Int) (hoho : Int)
deriving DecidableEq, Lean.ToJson

def x : Foo := Foo.Foo1 "hoho" "hehe"

#eval x == x
#eval Lean.ToJson.toJson x

[Eric Wieser]

Here's the lean translation of MyError

structure NameMessage where name : String; message : String
structure FooBar where foo : Int; bar : Int
abbrev MyError := Sum NameMessage FooBar

[Eric Wieser]

I think anonymous structures wouldn't be a great idea, because then you end up with MyError._anonstruct_1.name instead of NameMessage.name in the environment.

[Serhii Khoma (srghma)]

Eric Wieser said:

I think anonymous structures wouldn't be a great idea, because then you end up with MyError._anonstruct_1.name instead of NameMessage.name in the environment.

idris has

||| Get a field value by label
public export
get : (0 lbl:String) ->
      {0 f: FieldToType k} ->
      HasField lbl t r =>
      Record r f ->
      (f (lbl :->: t))

[Eric Wieser]

Sure, but the implementation of the HasField instance is still going to refer to the internal anonymous name,