Idris可以支持行多态吗？

Question

从而我可以构建一个匿名的临时记录; 这是可编辑的,可附加的,可修改的,其中每个值可以具有不同的异构类型,并且编译器检查消费者类型期望与所有给定键的生成记录的类型是否统一？

与Purescript支持的类似.

Answer 1

它可以,但标准库中没有一个模块,两个github项目gonzaw/extensible-records和jmars/Records似乎没有完全成熟/过时.

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

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

当然,你可以使用语法规则简化和美化这个很多.