Is there some way to hack the type system without recompiling GHC?
We know that the type system is now a second language where you spec formal requirements and let the compiler solve it, kinda like logic programming. But sometimes I knew something is correct or at least willing to take the risk of runtime errors, but the typechecker is not (yet) able to figure it out. In this case is it possible to somehow insert (regular haskell) code into the typechecker and force the compiler to think some values are of some types, rather than waiting for or inventing some formally correct solution, which may be fundamentally very difficult?
On Fri, Nov 23, 2018 at 02:11:29PM +0800, ducis wrote:
In this case is it possible to somehow insert (regular haskell) code into the typechecker
Are you looking for GHC plugins? https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/extending_ghc...
"force the compiler to think some values are of some types" Sounds like a job for unsafeCoerce. On Thu, Nov 22, 2018, 23:12 ducis <ducis_cn@126.com wrote:
We know that the type system is now a second language where you spec formal requirements and let the compiler solve it, kinda like logic programming. But sometimes I knew something is correct or at least willing to take the risk of runtime errors, but the typechecker is not (yet) able to figure it out. In this case is it possible to somehow insert (regular haskell) code into the typechecker and force the compiler to think some values are of some types, rather than waiting for or inventing some formally correct solution, which may be fundamentally very difficult?
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
Which is safe as long as the GC ETC still can walk it correctly! And that you’re not rereferencing an Int as a list of A :) On Sat, Nov 24, 2018 at 1:24 AM Dan Burton <danburton.email@gmail.com> wrote:
"force the compiler to think some values are of some types"
Sounds like a job for unsafeCoerce.
On Thu, Nov 22, 2018, 23:12 ducis <ducis_cn@126.com wrote:
We know that the type system is now a second language where you spec formal requirements and let the compiler solve it, kinda like logic programming. But sometimes I knew something is correct or at least willing to take the risk of runtime errors, but the typechecker is not (yet) able to figure it out. In this case is it possible to somehow insert (regular haskell) code into the typechecker and force the compiler to think some values are of some types, rather than waiting for or inventing some formally correct solution, which may be fundamentally very difficult?
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (4)
-
Carter Schonwald -
Dan Burton -
ducis -
Tom Ellis