Равенство значений не распространяется на типы в зависимости от этих значений; я что-то упускаю?

Я пытаюсь реализовать как можно больше System F (полиморфное лямбда-исчисление) в Idris. Теперь я столкнулся с проблемой, которую хочу продемонстрировать на примере:

data Foo = Bar Nat

Eq Foo where
 (Bar _) == (Bar _) = True

data Baz: Foo -> Type where
 Quux: (n: Nat) -> Baz (Bar n)

Eq (Baz f) where
 (Quux a) == (Quux b) = ?todo

Как видите, любые два значения Foo равны. Теперь я хотел бы иметь возможность использовать этот факт при определении равенства для Baz f: Quux a имеет тип Baz (Foo a), Quux b имеет тип Baz (Foo b), а Foo a и Foo b равны, так что моя интуиция подсказывает, что это должно работать. Но компилятор отказывается, говоря, что между Baz (Foo a) и Baz (Foo b) есть несоответствие типов.

Есть ли способ заставить это работать? Эта проблема мешает мне реализовать альфа-эквивалентность.


dependent-type idris
person Sebastian Zivota    schedule 16.09.2016    source источник
comment
Мой совет: не реализовывать альфа-эквивалентность   -  person Benjamin Hodgson♦    schedule 21.10.2016

Ответы (2)


arrow_upward
1
arrow_downward

К сожалению, я в основном не знаком с системой F и альфа-эквивалентностью, так что отнеситесь к этому с недоверием. Однако один из способов решить вашу проблему в конкретной ситуации, которую вы опубликовали, заключается в следующем:

data Foo = Bar

bar: Nat -> Foo
bar _ = Bar

Eq Foo where
 Bar == Bar = True

data Baz: Foo -> Type where
 Quux: (n: Nat) -> Baz (bar n)

Eq (Baz f) where
 (Quux a) == (Quux b) = ?todo

Насколько я понимаю, экземпляры Eq предназначены для проверки на равенство во время выполнения. С ними не консультируются, чтобы проверить, объединяются ли два типа.

Вы хотите, чтобы все экземпляры Foo были унифицированы на уровне типа, поэтому на самом деле может быть только один экземпляр; давайте просто назовем это Bar. Конструктор данных с таким именем, который у вас был в коде, был переведен в функцию bar, которая просто возвращает уникальный Foo экземпляр Bar для каждого Nat.

Реализация Eq для Foo теперь еще более тривиальна (хотя в данном случае она больше не нужна), а Quux теперь использует bar вместо Bar, так что все созданные им экземпляры Baz действительно имеют один и тот же тип Baz Foo.

person Julian Kniephoff    schedule 18.09.2016

arrow_upward
1
arrow_downward

Почему бы не определить другой оператор для разнородного равенства и использовать вместо него?

module Main

infix 5 ~=

interface HEq a b where
  (~=) : a -> b -> Bool

-- This will make ~= work as replacement for ==
Eq a => HEq a a where
  (~=) = (==)

data Foo = Bar Nat

Eq Foo where
  (Bar _) == (Bar _) = True

data Baz : Foo -> Type where
  Quux : (n : Nat) -> Baz (Bar n)

HEq (Baz a) (Baz b) where
  (Quux x) ~= (Quux y) = True -- do whatever you want here

main : IO Unit
main = do
  putStrLn $ show $ 5 ~= 5 -- prints True
  putStrLn $ show $ 5 ~= 6 -- prints False
  putStrLn $ show $ (Quux 10) ~= (Quux 20) -- prints True
person RKS    schedule 23.09.2016