Compiling GHC disabling the type checker
Hi, 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. Thanks Neil
| 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
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
FWIW, Lennart Augustsson's Cayenne compiler can compile to GHC
nowadays. It uses exactly this method of sprinkling coerce all over
the place to make GHC's typechecker happy.
http://www.augustsson.net/Darcs/Cayenne/
Cheers,
Josef
On 10/16/06, Simon Marlow
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
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.''
participants (5)
-
Josef Svenningsson -
Neil Mitchell -
roconnor＠theorem.ca -
Simon Marlow -
Simon Peyton-Jones