idris - 实现可扩展记录时出现编译错误
问题描述
我正在玩 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
我必须承认这个错误让我感到困惑。谁能解释这里发生了什么?
解决方案
似乎您是第一个在愤怒中使用该DecEq
实例的人String
,因此,您是第一个发现我们在这里为原语构建证明项的方式是错误的。对于那个很抱歉。好消息是它很容易修复(我刚刚在您的示例中尝试过,很好),坏消息是一旦我推动修复,您将需要 git head。
无论如何,我们迟到了一个新版本。这个周末我会尝试这样做。你的代码对我来说当然很好!
推荐阅读
- jasmine - 如何用茉莉花测试模拟函数的回调?
- python - 尝试根据另一列上的值分配标签,但始终获得相同的值
- crystal-reports - 如何在公式中包含函数文本?
- arduino - ')' 标记之前的 Arduino 错误预期主表达式
- swift - 无法分配给属性:“self”在 UIViewControllerRepresentable 中是不可变的
- typo3 - 重新激活 TYPO3 9 中的 saveDocView 按钮
- c++ - cpp 数据类型运行时溢出
- asp.net - Json POST 正文有时在服务器上被截断 - IIS 10.0 ASP.NET Core 3.0
- android - 无法在 9408 字节的 TensorFlowLite 缓冲区和 2352 字节的 ByteBuffer 之间进行转换
- android - 旋转屏幕时夜间模式出错