
8 Dec
2005
8 Dec
'05
11:56 p.m.
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/TR... 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