Gleichheit der Werte überträgt sich nicht auf Typen, die von diesen Werten abhängen; Fehle ich etwas?

Question

Ich versuche, so viel von System F (polymorphe Lambda-Kalkül) zu implementieren, wie ich in Idris kann. Ich bin jetzt mit einem Problem konfrontiert, dass ich mit einem Beispiel demonstrieren will:

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 

Wie Sie sehen können, wird alle zwei Foo Werte gleich sind. Ich würde jetzt in der Lage sein mag, diese Tatsache zu nutzen, während Gleichheit auf Baz f definieren: Quux a hat Baz (Foo a) geben, hat Quux bBaz (Foo b) eingeben und Foo a und Foo b gleich sind, so meine Intuition ist, dass dies funktionieren soll. Aber der Compiler lehnt es ab und sagt, dass es einen Typ-Mismatch zwischen Baz (Foo a) und Baz (Foo b) gibt.

Gibt es eine Möglichkeit, dies zu erreichen? Dieses Problem hindert mich daran, die Alpha-Äquivalenz zu implementieren.

Answer 1

Leider bin ich meistens ignorant von System F und Alpha-Äquivalenz, also nehmen Sie das mit einem Körnchen Salz. Allerdings ist ein Weg, um Ihr Problem in der jeweiligen Situation zu beheben Sie geschrieben, ist dies:

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 

Soweit ich es verstehe, Eq Instanzen sind für die Gleichstellung Kontrollen an Laufzeit. Sie werden nicht konsultiert, um zu überprüfen, ob sich zwei Typen vereinheitlichen.

Sie möchten, dass alle Foo Instanzen auf der Typenebene vereinheitlichen, also kann es nur eine geben; Lass es uns einfach Bar nennen. Der Datenkonstruktor dieses Namens, den Sie in Ihrem Code hatten, wurde auf eine Funktion bar verwiesen, die nur die eindeutige Foo Instanz Bar für jeden Nat zurückgibt.

Die Eq Implementierung für Foo ist noch trivial jetzt (auch wenn es nicht mehr in diesem Fall benötigt wird) und Quux verwendet jetzt bar statt Bar, so dass die alle Baz Instanzen von ihr geschaffenen wirklich Baz Foo die gleiche Art teilen.

Answer 2

Warum nicht einen anderen Operator für heterogene Gleichheit definieren und stattdessen verwenden?

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