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.
Have a look at these:
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/open-witness
--
Ashley Yakeley
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
