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

Question

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

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).

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

Answer 1

К сожалению, я в основном не осведомлен о системе 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, которая возвращает уникальный экземпляр FooBar за каждые Nat.

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

Answer 2

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

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