RE: Compiling GHC disabling the type checker
| How does GHC react to a really large number of unsafeCoerce's? Is this | likely to destroy performance? Has anything like this been done | before? I know that LML was able to turn off the type checker, but I | guess GHC doesn't have such an option, because of its typed Core | language. I've never tried that. However GHC now handles 'casts' in a more systematic way (this is the FC stuff), and I hitnk unsafe coerces will benefit from that. Worth a try. Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Compiling GHC disabling the type checker
Neil Mitchell wrote:
I would like to write a translator which takes a Haskell-like language
to GHC compilable Haskell. This Haskell-like language is not
explicitly typed, and cannot have types inferred for it (rank 2 types
may exist etc), however it is known that the program will not crash
with a type error. All case statements are well typed, i.e. case x of
{1 - ..; True - ...} will not happen, although types cannot be given
to the whole program.
How does GHC react to a really large number of unsafeCoerce's? Is this
likely to destroy performance? Has anything like this been done
before? I know that LML was able to turn off the type checker, but I
guess GHC doesn't have such an option, because of its typed Core
language.
There's one restriction that I know of: you should be careful not to cast a
function value to a non-function type (except a polymorphic type), because the
two have incompatible representations when it comes to seq and case. And of
course, you should never cast an unboxed value to a boxed type or vice versa.
Apart from these, I think you should be fine to unsafeCoerce# away.
Cheers,
Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Compiling GHC disabling the type checker
On Mon, 16 Oct 2006, Simon Marlow wrote: There's one restriction that I know of: you should be careful not to cast a function value to a non-function type (except a polymorphic type), because the two have incompatible representations when it comes to seq and case. And of course, you should never cast an unboxed value to a boxed type or vice versa. Apart from these, I think you should be fine to unsafeCoerce# away. Coq's extraction mechinism uses the type () whenever it encounters a dependent type that it cannot make a Haskell type for. Thus, all sorts of functions end up getting cast to () types. Would it be safer to cast things to ``() - ()'', or perhaps a single polymorphic variable ``a''? -- 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.'' ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
