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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
