Re: Type checker plugins

Hi, It shouldn't be hard to do the merge, but I am not sure that I'll have time to do it before the weekend---I'll give it a go then. -Iavor On Tue, Oct 21, 2014 at 9:40 AM, Adam Gundry wrote: > Thanks Iavor, this is really helpful! > > If you have a moment to merge Simon's more recent changes

Re: Type checker plugins

Thanks Iavor, this is really helpful! If you have a moment to merge Simon's more recent changes on wip/new-flatten-skolems-Aug14, I'm keen to try out the new unflattening... or I can have a go at the merge if it would help? You may be right that flattened constraints are easier to work with in so

Re: Type checker plugins

Hello, Just a heads up, if anyone is playing around with this: I just updated the plugin interface a bit. Here are the changes: - A plugin now gets 3 sets of constraints: given, derived, and wanted (in that order) - Plugins are now also presented with dictionary constraints (i.e., you may

Re: Type checker plugins

Hello, On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry wrote: > > > One problem I've run into is transforming the flattened CFunEqCans into > unflattened form (so the flatten-skolems don't get in the way of > AG-unification). Do you know if there is an easy way to do this, or do I > need to rebuild

RE: Type checker plugins

checker plugins | | Ok, I hadn't realised that. Looking in the user's guide, I see <= and | <=? for Nat, but I couldn't find anything about Symbol. I must try | them out! | | | > From: Carter Schonwald | > | > the alphabetical ordering on Symbol is a

Re: Type checker plugins

mind you, i'm not sure what the ordering is specified to be :) On Thu, Oct 16, 2014 at 9:24 PM, Carter Schonwald < carter.schonw...@gmail.com> wrote: > http://hackage.haskell.org/package/base-4.7.0.1/docs/GHC-TypeLits.html > > type family CmpSymbol m n :: Ordering >

Re: Type checker plugins

http://hackage.haskell.org/package/base-4.7.0.1/docs/GHC-TypeLits.html type family CmpSymbol m n :: Ordering On Thu, Oct 16, 2014 at 7:14 PM, Barney Hilken wrote: > Ok, I hadn't realised that. Looking in the user's

Re: Type checker plugins

Ok, I hadn't realised that. Looking in the user's guide, I see <= and <=? for Nat, but I couldn't find anything about Symbol. I must try them out! > From: Carter Schonwald > > the alphabetical ordering on Symbol is already exposed via TypeLits... this > would be some machinery to help maintai

Re: Type checker plugins

the alphabetical ordering on Symbol is already exposed via TypeLits... this would be some machinery to help maintain that ordering with less user intervention? On Thu, Oct 16, 2014 at 6:59 PM, Barney Hilken wrote: > I can think of a use for a non-equality constraint: an alphabetical > ordering o

Re: Type checker plugins

I can think of a use for a non-equality constraint: an alphabetical ordering on Symbol. This would allow experimental implementations of extensible records (without shadowing) which keep the labels sorted. An order constraint on Nat might be useful, too. Barney. ___

RE: Type checker plugins

:a...@well-typed.com] | Sent: 16 October 2014 21:50 | To: Eric Seidel; Simon Peyton Jones | Cc: Iavor Diatchki; glasgow-haskell-users@haskell.org | Subject: Re: Type checker plugins | | Thanks Simon, your branch does make it a lot more feasible to unflatten, | so I'll just go ahead and implement th

Re: Type checker plugins

ell.org] On Behalf Of Adam Gundry >> | Sent: 16 October 2014 11:59 >> | To: Iavor Diatchki >> | Cc: glasgow-haskell-users@haskell.org >> | Subject: Re: Type checker plugins >> | >> | Hi Iavor, >> | >> | >> | On 13/10/14 21:34, Iavor Diatchki w

RE: Type checker plugins

t: 16 October 2014 11:59 | To: Iavor Diatchki | Cc: glasgow-haskell-users@haskell.org | Subject: Re: Type checker plugins | | Hi Iavor, | | | On 13/10/14 21:34, Iavor Diatchki wrote: | > Hello, | > | > We now have an implementation of type-checker with plugin support. | I

Re: Type checker plugins

Hi Iavor, On 13/10/14 21:34, Iavor Diatchki 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 Thanks, this is great! I'd been working on a similar imp

Re: Type checker plugins

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 wrote: > Hello, > > We now have an implementation of type-checker with plugin support. If you > are interested

Re: Type checker plugins

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://gi

Re: Type checker plugins

yay :) On Mon, Oct 6, 2014 at 2:42 PM, Iavor Diatchki 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 wrote: > >> Hi folks, >> >> Those of

Re: Type checker plugins

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 wrote: > Hi folks, > > Those of you at HIW last week might have been subjected to my lightning > talk on plugins fo

Re: Type checker plugins

i'm looking at the record type data TcPlugin = forall t . TcPlugin { init :: TcM t , solve :: t -> [Ct] -> [Ct] -> TcS ([SolveResult], [Ct]) , close :: t -> TcM () } it might be helpful to add a remark that data Ct = ... is defined in compiler/typechecker/TcRnTypes.lhs so folks who aren'

Type checker plugins

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 id