Type checker plugins

[Austin Seipp]

Iavor,

Wow, this is one of the coolest new features I've seen in a while, I
have to say. I hope we can see it in GHC sometime soon. :)

On Mon, Oct 13, 2014 at 3:34 PM, Iavor Diatchki
<iavor.diatchki at gmail.com> wrote:
> 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
>>>
>>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>



-- 
Regards,

Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/