data (a :=: a') where Refl :: a :=: a Comm :: (a :=: a') -> (a' :=: a) Trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'') Martijn van Steenbergen wrote:
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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe