Equality of values doesn't carry over to types depending on those values; am I missing something?

3
votes

I'm trying to implement as much of System F (polymorphic lambda calculus) as I can in Idris. I'm now faced with a problem that I want to demonstrate with an example:

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

As you can see, any two Foo values are equal. I would now like to be able to use this fact while defining equality on Baz f: Quux a has type Baz (Foo a), Quux b has type Baz (Foo b), and Foo a and Foo b are equal, so my intuition is that this should work. But the compiler refuses it, saying there's a type mismatch between Baz (Foo a) and Baz (Foo b).

Is there a way to make this work? This issue is stopping me from implementing alpha equivalence.

2
dependent-typeidris
My advice is not to implement alpha equivalence – Benjamin Hodgson

2 Answers

1
votes

Unfortunately I am mostly ignorant of system F and alpha equivalence, so take this with a grain of salt. However, one way to fix your problem in the particular situation you posted is this:

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

As far as I understand it, Eq instances are for equality checks at runtime. They are not consulted to check whether two types unify.

You want all Foo instances to unify on the type level, so there can actually only be one; let's just call it Bar. The data constructor of that name, that you had in your code, was relegated to a function bar, that just returns the unique Foo instance Bar for every Nat.

The Eq implementation for Foo is even more trivial now (although it is no longer needed in this case) and Quux now uses bar instead Bar, so all the Baz instances created by it really share the same type Baz Foo.

1
votes

Why not define another operator for heterogenous equality and use that instead ?

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