proposal: add 'unsafeCoerce'

roconnor at theorem.ca roconnor at theorem.ca
Sun Nov 19 05:28:11 EST 2006


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.''


More information about the Libraries mailing list