Ralf Hinze wrote:
the type a :=: b defined below
goes back to  Leibniz's principle of substituting equals for equals:

If you like this, check out two of Ralf's papers:

First-class phantom types:
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901
Fun with phantom types:
http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf

The first (in section 2.4) explains a limitation of :=:

I highly recommend both papers.

Jim

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to