实现可扩展记录时出现编译错误

Question

我正在研究 idris 并试图实现可扩展记录。

主要目标是保证记录的键是唯一的。

例如

("Year" := 1998) +: rnil

合法

("Title" := "test") +: ("Year" := 1998) +: rnil

也可以，但是

("Year" := "test") +: ("Year" := 1998) +: rnil

应该编译失败。

我想出了以下编译良好的实现：

{-
See: http://lpaste.net/104020
  and https://github.com/gonzaw/extensible-records
-}
module Record

import Data.List

%default total

data HList : List Type -> Type where
  Nil : HList []
  (::) : a -> HList xs -> HList (a :: xs)

infix 5 :=

data Field : lbl -> Type -> Type where
  (:=) : (label : lbl) ->
          (value : b) -> Field label b

labelsOf : List (lbl, Type) -> List lbl
labelsOf [] = []
labelsOf ((label, _) :: xs) = label :: labelsOf xs

toFields : List (lbl, Type) -> List Type
toFields [] = []
toFields ((l, t) :: xs) = (Field l t) :: toFields xs

data IsSet : List t -> Type where
  IsSetNil : IsSet []
  IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)

data Record : List (lty, Type) -> Type where
  MkRecord : IsSet (labelsOf ts) -> HList (toFields ts) ->
                                    Record ts

infixr 6 +:

rnil : Record []
rnil = MkRecord IsSetNil []

prepend : { label : lbl,
          xs : List (lbl, Type),
          prf : Not (Elem label (labelsOf xs))
        } ->
        Field label t ->
        Record xs ->
        Record ((label, t) :: xs)
prepend {prf} f (MkRecord isSet fs) = MkRecord (IsSetCons prf isSet) (f :: fs)

data IsNo : Dec prop -> Type where
  ItIsNo : IsNo (No y)

(+:) : DecEq lbl =>
  { label : lbl, xs : List (lbl, Type) } ->
  Field label t ->
  Record xs ->
  { auto isno : IsNo (isElem label $ labelsOf xs) } ->
  Record ((label, t) :: xs)

(+:) {label} {xs} f r with (isElem label $ labelsOf xs)
    (+:) { isno = ItIsNo } _ _ | (Yes _) impossible
    (+:) f r | (No no) = prepend {prf = no} f r

有趣的一点是

  { auto isno : IsNo (isElem label $ labelsOf xs) } ->

这个想法是，如果键是唯一的，编译器将轻松找到 IsNo 的实例，而如果键不是唯一的，编译器将无法找到它，因此无法编译。

这对那些例子很有效

("Year" := 1998) +: rnil                       -- Compiles fine
("Year" := "test") +: ("Year" := 1998) +: rnil -- fails to compile as expected

但是

("Title" := "test") +: ("Year" := 1998) +: rnil

编译失败，出现以下错误：

    (input):Type mismatch between
        ("Title" = "Year") -> "Title" = "Year"
and
        ("Title" = "Year") -> Void

我必须承认这个错误让我很困惑。谁能解释这里发生了什么？

Answer 1

看来您是第一个在愤怒中使用 DecEq 实例作为 String 的人，因此，您是第一个发现我们为这里的原语是错误的。对于那个很抱歉。好消息是它很容易修复（我刚刚在你的例子中试过了，没问题），坏消息是一旦我推动了修复，你将需要 git 头。

无论如何我们都应该发布新版本了。这个周末我会努力做到这一点。你的代码对我来说当然没问题！

实现可扩展记录时出现编译错误

Compilation error while implementing extensible record

idris