Olá café, With the recent generic programming work and influences from type-dependent languages such as Agda, the following data type seems to come up often:
data (a :=: a') where Refl :: a :=: a
Everyone who needs it writes their own version; I'd like to compile a package with this data type and related utilities, if such a package doesn't exist already (I couldn't find one). Below is what I have so far; I'd much appreciate it if you added your ideas of what else the package should contain.
{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-}
module Eq where
data (a :=: a') where Refl :: a :=: a
class Eq1 f where eq1 :: f a -> f a' -> Maybe (a :=: a')
class Eq2 f where eq2 :: f a b -> f a' b' -> Maybe (a :=: a', b :=: b')
class Eq3 f where eq3 :: f a b c -> f a' b' c' -> Maybe (a :=: a', b :=: b', c :=: c')
Thank you, Martijn.