Тип данных, который представляет доказательство того, что две функции эквивалентны - PullRequest
Новая
       11

Тип данных, который представляет доказательство того, что две функции эквивалентны

0 голосов
/ 22 ноября 2018

Я пытался создать тип данных, отражающий тот факт, что две функции эквивалентны.Что означает ошибка?

Код: 

record FEq (f1 : a -> b) (f2 : a -> b) where
    constructor MkFEq
    unFEq : (x : a) -> (f1 x = f2 x)

Ошибка: 

Type checking ./FEq.idr
FEq.idr:1:1-3:36:
  |
1 | record FEq (f1 : a -> b) (f2 : a -> b) where
  | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking type of Main.FEq.unFEq:
When checking argument x to type constructor =:
        Type mismatch between
                free_a b a f1 f2 rec
        and
                a

1 Ответ

0 голосов
/ 24 ноября 2018

AFAIK Вы не можете упоминать несвязанные параметры в записи.Таким образом, вы должны добавить a и b в качестве параметров, например, так: 

record FEq a b (f1 : a -> b) (f2 : a -> b) where
  constructor MkFEq
  unFEq : (x : a) -> (f1 x = f2 x)
...