I use these defs:<br><br><span style="font-family: courier new,monospace;">-- | Lift proof through a unary type constructor</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">liftEq :: a :=: a' -> f a :=: f a'</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">liftEq Refl = Refl</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- | Lift proof through a binary type constructor (including '(,)')</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">liftEq2 :: a :=: a' -> b :=: b' -> f a b :=: f a' b'</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">liftEq2 Refl Refl = Refl</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- | Lift proof through a ternary type constructor (including '(,,)')</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">liftEq3 :: a :=: a' -> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c'</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">liftEq3 Refl Refl Refl = Refl</span><br>
<br>etc.<br><br><br><br><div class="gmail_quote">On Tue, Mar 17, 2009 at 3:39 AM, Martijn van Steenbergen <span dir="ltr"><<a href="mailto:martijn@van.steenbergen.nl">martijn@van.steenbergen.nl</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Olá café,<br>
<br>
With the recent generic programming work and influences from type-dependent languages such as Agda, the following data type seems to come up often:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
data (a :=: a') where<br>
Refl :: a :=: a<br>
</blockquote>
<br>
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.<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
{-# LANGUAGE GADTs #-}<br>
{-# LANGUAGE TypeOperators #-}<br>
<br>
module Eq where<br>
<br>
data (a :=: a') where<br>
Refl :: a :=: a<br>
<br>
class Eq1 f where<br>
eq1 :: f a -> f a' -> Maybe (a :=: a')<br>
<br>
class Eq2 f where<br>
eq2 :: f a b -> f a' b' -> Maybe (a :=: a', b :=: b')<br>
<br>
class Eq3 f where<br>
eq3 :: f a b c -> f a' b' c' -> Maybe (a :=: a', b :=: b', c :=: c')<br>
</blockquote>
<br>
Thank you,<br>
<br>
Martijn.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>