Type checker plugins

Iavor Diatchki iavor.diatchki at gmail.com
Mon Oct 13 20:34:16 UTC 2014


Hello,

We now have an implementation of type-checker with plugin support.   If you
are interested in trying it out:

  - Checkout and build the `wip/tc-plugins` branch of GHC

  - As an example, I've extracted my work on using an SMT solver at the
type level as a separate plugin:

      https://github.com/yav/type-nat-solver

   - To see how to invoke a module that uses a plugin, have a look in
`examples/A.hs`.
     (Currently, the plugin assumes that you have `cvc4` installed and
available in the path).

    - Besides this, we don't have much documentation yet.  For hackers: we
tried to use `tcPlugin` on
    `TcPlugin` in the names of all things plugin related, so you could grep
for this.  The basic API
     types and functions are defined in `TcRnTypes` and `TcRnMonad`.

Happy hacking,
-Iavor











On Mon, Oct 6, 2014 at 11:53 AM, Carter Schonwald <
carter.schonwald at gmail.com> wrote:

> yay :)
>
> On Mon, Oct 6, 2014 at 2:42 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
>> Hi Adam,
>>
>> I am back from vacation, and I think I should have some time to try to
>> implement something along these lines.
>>
>> Cheers,
>> -Iavor
>>
>> On Fri, Sep 12, 2014 at 9:41 AM, Adam Gundry <adam at well-typed.com> wrote:
>>
>>> Hi folks,
>>>
>>> Those of you at HIW last week might have been subjected to my lightning
>>> talk on plugins for the GHC type checker, which should allow us to
>>> properly implement nifty features like units of measure or type-level
>>> numbers without recompiling GHC. I've written up a wiki page summarising
>>> the idea:
>>>
>>> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker
>>>
>>> Feedback is very welcome, particularly if (a) you have an interesting
>>> use for this feature or (b) you think this is a terrible idea!
>>>
>>> Thanks,
>>>
>>> Adam
>>>
>>>
>>> --
>>> Adam Gundry, Haskell Consultant
>>> Well-Typed LLP, http://www.well-typed.com/
>>>
>>
>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20141013/802edc77/attachment.html>


More information about the Glasgow-haskell-users mailing list