workaround to get both domain-specific errors and also multi-modal type inference?
Nicolas Frisby
nicolas.frisby at gmail.com
Tue Feb 11 18:55:51 UTC 2014
If, when defining the `describeError' method, I wanted to refer to one of
my library's classes from inside a pattern (or guard in the rhs, I
suppose), how would I do that? Via a Template Haskell literal name? Or
would I call the TcM interface for looking up a name?
In my opinion [1], the TcM interface is too user-antagonistic, even for GHC
power-users [2], and moreover would leak implementation details. I would
prefer a more light-weight interface, dedicated to just domain-specific
errors.
That said, it seems that a general interface comparable to the one I have
been hocking could be built atop what you two are proposing and
subsequently marked {-# LANGUAGE Trustworthy #-}. Thumbs up.
[1] - Disclaimer: I've already noted that I'm not familiar with the
type-checker implementation.
[2] - I consider myself a GHC power-user.
On Tue, Feb 11, 2014 at 12:43 PM, Adam Gundry <adam at well-typed.com> wrote:
> Thanks for clarifying, Richard, I should have been clearer. "Constraint"
> was a poor choice of type without further explanation.
>
> Nicolas, Pedro, thanks for your feedback!
>
> On 11/02/14 18:24, Nicolas Frisby wrote:
> > Thanks for suggesting that; I was only seeing Constraint as in
> > ConstraintKinds.
> >
> > I think the gist of my previous concerns doesn't change, though: open
> > type pattern matching (or some dissatisfying approx of), assuredly pure
> > functions, etc.
>
> The point of doing it this way - effectively hooking code into GHC - is
> that the error-reporting code would work with the GHC internal
> representation of constraints, thereby avoiding trouble with open types.
> The GHC API can be used to decompose the constraint type. This would
> make it much easier to do complex processing than trying to write tricky
> functional programs with type families. We might also want the
> error-reporting function to live in GHC's TcM monad so it has access to
> whatever state it wanted.
>
> Cheers,
>
> Adam
>
> [Resent to ghc-devs from the correct email address.]
>
>
> > On Feb 11, 2014 12:15 PM, "Richard Eisenberg" <eir at cis.upenn.edu
> > <mailto:eir at cis.upenn.edu>> wrote:
> >
> > One potential source of confusion in this thread:
> >
> > When Adam initially suggested a function (Constraint -> Maybe
> > String), I believe he was referring to constraints as they slosh
> > around within GHC, *not* the kind-level Constraint available with
> > ConstraintKinds. So, the error-reporting function would be written
> > in a separate module from the code it affects, and it would be
> > imported somewhat like Template Haskell does. Then, GHC could call
> > the function when type inference fails. This would make programming
> > the interface much easier and more expressive.
> >
> > Please correct me if I'm wrong, but it seemed that different people
> > were talking about different solutions!
> >
> > Richard
> >
> > On Feb 11, 2014, at 11:10 AM, Nicolas Frisby
> > <nicolas.frisby at gmail.com <mailto:nicolas.frisby at gmail.com>> wrote:
> >
> >> On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães
> >> <jpm at cs.uu.nl <mailto:jpm at cs.uu.nl>> wrote:
> >>
> >> On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby
> >> <nicolas.frisby at gmail.com <mailto:nicolas.frisby at gmail.com>>
> >> wrote:
> >>
> >> > type family GHC.Exts.Message (c :: Constraint) :: Maybe
> >> Symbol
> >>
> >> While I do find this problem very relevant, and think this
> >> solution is going in the right direction,
> >> I'm afraid it's not that simple. Say I have
> >>
> >> type instance Message (MyClass a) = Just ...
> >>
> >> How will this behave if the unsatisfied constraint is of the
> >> form (C b, MyClass a)? How about
> >> f (MyClass a), for some f :: Constraint -> Constraint?
> >>
> >> Also, isn't it a bit unsatisfying that an instance such as
> >>
> >> type instance Message a = Just ...
> >>
> >> would pollute error messages everywhere?...
> >>
> >>
> >> Hi Pedro. Very glad you're joining in.
> >>
> >> Thank you for the helpful observations. I see two options.
> >>
> >> 1) Keep it simple at first. EG An unsatisfied conjunction is
> >> decompose into a list of its unsatisfied conjuncts before ab
> >> Message is ever sought. Similarly, only support matching the head
> >> of the unsatisfied constraint, so the Message pattern would have
> >> to match (F (MyClass a)), for whichever F is your `f'. And so on.
> >> Lastly, we might consider allowing type class-like overlap for
> >> instances of the Message family, since it's use-case is so specific.
> >>
> >> These limits each restrict the expressivity but deserve
> >> investigation regarding how much mileage we can get out of them.
> >>
> >> 2) Or we could design a type-level DSL for querying the "trace" of
> >> the constraint-solver that ended up with this unsatisfied
> >> constraint. This sounds much harder to me, since I'm unfamiliar
> >> with the solver and its internals. But it seems like the way to
> >> maximize expressitivity.
> >>
> >> -----
> >>
> >> I should point out that I think the courageous library designer
> >> could squeeze some of the functionality of (2) out of (1), at the
> >> cost of obfuscation. For example:
> >>
> >> > class Constraint a b where -- this is the actual class of interest
> >> >
> >> > data Trace = forall a b. Start a b | ...
> >> >
> >> > instance InternalConstraint (Start a b) a b => Constraint a b
> >> >
> >> > class InternalConstraint trace x y -- all instances are
> >> parametric wrt `trace'
> >> >
> >> > -- I'm assuming Message has range Maybe Doc, where GHC
> >> interprets Doc to build an error message.
> >> > type instance Message (InternalConstraint a b x y) =
> >> > Just ( Text "While solving Constraint for " <> ShowType a
> >> <> Text " and " <> ShowType b
> >> > <> Text " the point of failure was " <> ShowType x <>
> >> Text " and " <> ShowType y <> Text "."
> >> > )
> >> _______________________________________________
> >> ghc-devs mailing list
> >> ghc-devs at haskell.org <mailto:ghc-devs at haskell.org>
> >> http://www.haskell.org/mailman/listinfo/ghc-devs
> >
> >
> >
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://www.haskell.org/mailman/listinfo/ghc-devs
> >
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140211/1754d1cd/attachment-0001.html>
More information about the ghc-devs
mailing list