Can Idris support row-polymorphism?

Question

Whereby I could construct an anonymous, ad-hoc record; that's editable, appendable, modifiable, where each value can have different heterogenous type, and where the compiler checks that the consumers type expectations unify with the types of the produced record at all the given keys?

Similar to what Purescript supports.

xash xash · Accepted Answer · 2018-04-19T10:09:22

It could, but there isn't a module in the standard library, and the two github projects gonzaw/extensible-records and jmars/Records don't seem to be full-fledged/outdated.

You might need to implement it for yourself. The rough idea is:

import Data.Vect

%default total

data Record : Vect n (String, Type) -> Type where
  Empty : Record []
  Cons : (key : String) -> (val : a) -> Record rows -> Record ((key, a) :: rows)

delete : {k : Vect (S n) (String, Type)} -> (key : String) ->
       Record k -> {auto prf : Elem (key, a) k} -> Record (Vect.dropElem k prf)
delete key (Cons key val r) {prf = Here} = r
delete key (Cons oth val Empty) {prf = (There later)} = absurd $ noEmptyElem later
delete key (Cons oth val r@(Cons x y z)) {prf = (There later)} =
  Cons oth val (delete key r)

update : (key : String) -> (new : a) -> Record k -> {auto prf : Elem (key, a) k} -> Record k
update key new (Cons key val r) {prf = Here} = Cons key new r
update key new (Cons y val r) {prf = (There later)} = Cons y val $ update key new r

get : (key : String) -> Record k -> {auto prf : Elem (key, a) k} -> a
get key (Cons key val x) {prf = Here} = val
get key (Cons x val y) {prf = (There later)} = get key y

With this we can write functions that handle fields without knowing the full record type:

rename : (new : String) -> Record k -> {auto prf : Elem ("name", String) k} -> Record k
rename new x = update "name" new x

forgetAge : Record k -> {auto prf : Elem ("age", Nat) k} -> Record (dropElem k prf)
forgetAge k = delete "age" k

getName : Record k -> {auto prf : Elem ("name", String) k} -> String
getName r = get "name" r

S0 : Record [("name", String), ("age", Nat)]
S0 = Cons "name" "foo" $ Cons "age" 20 $ Empty

S1 : Record [("name", String)]
S1 = forgetAge $ rename "bar" S0

ok1 : getName S1 = "bar"
ok1 = Refl

ok2 : getName S0 = "foo"
ok2 = Refl

Of course you can simplify and prettify this alot with syntax rules.

Can Idris support row-polymorphism?

1 Answers