19 Nov
2006
19 Nov
'06
5:28 a.m.
On Fri, 17 Nov 2006, Ross Paterson wrote:
So presumably Neil and Don think there are situations where it can be safely used across implementations. What are they?
Coq's Haskell extraction uses unsafe coerce to defeat the type system. Some of Coq's dependent types are difficult to represent in Haskell (such as (\n -> (Bool -> ... (n times) ... -> Bool)). So it uses unsafeCoerce to get around this. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''