Ошибка компиляции при реализации расширяемой записи - PullRequest
Новая
       7

Ошибка компиляции при реализации расширяемой записи

0 голосов
/ 26 мая 2018

Я играю с 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

Я должен признать, что эта ошибка сбивает меня с толку.Кто-нибудь может объяснить, что здесь происходит?

1 Ответ

0 голосов
/ 26 мая 2018

Кажется, что вы первый, кто использовал экземпляр DecEq для String в гневе, и, как следствие, вы первый, кто обнаружил, что способ построения терминов доказательства для примитивов здесь неправильный.Извини за это.Хорошая новость заключается в том, что это легко исправить (я только что попробовал это на вашем примере, и это нормально), плохая новость в том, что вам понадобится git head, как только я нажму исправление.

Мы все еще не успели выпустить новую версию.Я постараюсь сделать это в эти выходные.Ваш код, безусловно, выглядит хорошо для меня!

...