Idris 可以支持行多态吗？

Question

由此我可以构建一个匿名的临时记录；那是可编辑的、可附加的、可修改的，其中每个值可以具有不同的异构类型，并且编译器会检查消费者的类型期望是否与所有给定键处生成的记录的类型一致？

类似于 Purescript 所支持的。

Answer 1

可以，但标准库中没有模块，gonzaw/extensible-records 和 jmars/Records 两个 github 项目似乎并不成熟/过时。

您可能需要自己实现它。粗略的想法是：

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

有了这个，我们可以编写处理字段而不知道完整记录类型的函数：

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

当然，你可以通过语法规则来简化和美化它。