workaround to get both domain-specific errors and also multi-modal type inference?
José Pedro Magalhães
jpm at cs.uu.nl
Tue Feb 11 09:55:19 UTC 2014
On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <nicolas.frisby at gmail.com>wrote:
> Hi Adam. Thanks very much for the response. I'm sorry if the rest of this
> reads negatively -- I'm on my phone and hence perhaps curt. I'm excited
> about any dialog here!
>
> (I'll mention that Dimitrios Vytiniotis and Geoffrey Mainland had
> expressed low priority interest in these topics about a year ago.)
>
> I agree that this is a difficult problem. I think the eventual solution
> deserves far more attention than I can currently allocate. Hence, I was
> hoping for a workaround "trick" in the mean time.
>
> It seems to me that such a trick is currently unlikely. So I proposed a
> light-weight limited-scope patch. Something along the lines of "don't let
> perfect be the enemy of good."
>
> My main concern with the interface you sketched is how we would pattern
> match on the demoted Constraint, since Constraint is an open kind. Also,
> there's unsafePerformIO et al to somehow preclude. The interface does look
> nicer that way, but it would be simpler to stick to type-level computation,
> where no "exotic" new mechanisms would be needed.
>
> Maybe there's a middle ground.
>
> > 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?...
Cheers,
Pedro
> GHC would report the result of this family for any unsatisfied constraint
> that has a matching instance that returns Just msg.
>
> Perhaps GHC even first replaces skolem type variables with an application
> of GHC.Exts.Skolem :: Symbol -> k -> k before checking for instances.
>
> Of course, the Symbol operations are rather anemic at the moment, but I
> think improvements there would be valuable as well. Or perhaps Message
> could yield a type-level Doc data kind that GHC interprets to build a
> String.
>
> Lastly, I think custom constraint solving sounds like a very delicate
> language extension, with wide reaching consequences. Unless there's a
> strong champion dedicated to extensible custom constraint solving, I hope
> the much more modestly scoped issue of custom error messages can be
> considered separately for at least one design iteration. I feel like a
> near-term implementation is more likely that way.
>
> Thanks again for this conversation!
> On Feb 7, 2014 2:05 PM, "Adam Gundry" <adam at well-typed.com> wrote:
>
>> Hi,
>>
>> Good error messages are a hard problem. That said, I think little tweaks
>> like this might make sense. Richard Eisenberg and I were discussing this
>> earlier, and we wondered if the following might provide an alternative
>> approach:
>>
>> Suppose a module provides a function
>>
>> describeError :: Constraint -> Maybe String
>>
>> (exact type up for discussion). This could be called by the typechecker
>> when reporting errors in other modules, to provide a domain-specific
>> error message. Do you think this might work for your use case?
>>
>> We need to think about how to mark this function as special: one option
>> is to provide a built-in typeclass like
>>
>> class TypeCheckerPlugin a where
>> describeError :: Constraint -> Maybe String
>>
>> and look for instances of this class. Interestingly, the class type is
>> irrelevant here; we're not interested in solving constraints involving
>> this class, just looking at the imported instances when running the
>> typechecker. Perhaps using a pragma might be more principled.
>>
>> This came up in the context of a more general discussion of plugins to
>> extend the typechecker. For example, we might consider doing something
>> similar to *solve* constraints in a domain-specific way, as well as
>> reporting errors.
>>
>> Sound plausible?
>>
>> Adam
>>
>>
>> On 30/01/14 21:09, Nicolas Frisby wrote:
>> > Also, on the topic of patching GHC for domain-specific error messages,
>> > why not add a simple means to emit a custom error message? It would beat
>> > piggy-backing on the "no instance" messages as I currently plan to.
>> >
>> > This seems safe and straight-forward:
>> >
>> >> -- wired-in, cannot be instantiated
>> >> class GHC.Exts.PrintError (msg :: Symbol) (args :: [k])
>> >
>> > Consider the class C fromy previous email. It's possible these two
>> > instances are now sufficient.
>> >
>> >> instance C a b
>> >> instance PrintError ("You used %1 on the left and %2 on the right!" ::
>> > Symbol) [a,b] => C a b
>> >
>> > And let's not forget warnings!
>> >
>> >> -- wired-in, cannot be instantiated
>> >> class GHC.Exts.PrintWarn (msg :: Symbol) (args :: '[k])
>> >
>> > Thanks again.
>> >
>> >
>> > On Thu, Jan 30, 2014 at 3:07 PM, Nicolas Frisby
>> > <nicolas.frisby at gmail.com <mailto:nicolas.frisby at gmail.com>> wrote:
>> >
>> > Hi all. I have a question for those savvy to the type-checker's
>> > internal workings.
>> >
>> > For uses of the following function, can anyone suggest a means of
>> > forcing GHC to attempt to solve C a b even if a~b fails?
>> >
>> > > dslAsTypeOf :: (C a b,a~b) => a -> b -> a
>> > > dslAsTypeOf x _ = x
>> > >
>> > > class C a b -- no methods
>> >
>> > Just for concreteness, the following are indicative of the variety
>> > of instances that I expect C to have. (I don't think this actually
>> > affects the question above.)
>> >
>> > > instance C DSLType1 DSLType1
>> > > instance C DSLType2 DSLType2
>> > > instance C x y => C (DSLType3 x) (DSLType3 y)
>> > >
>> > > instance IndicativeErrorMessage1 => C DSLType1 DSLType2
>> > > instance IndicativeErrorMessage2 => C DSLType2 (DSLType3 y)
>> > >
>> > > class IndicativeErrorMessage1 -- will never have instances
>> > > class IndicativeErrorMessage2 -- will never have instances
>> >
>> > Thank you for your time.
>> >
>> > ===================================
>> >
>> > Keep reading for the "short story", the "long story", and two ideas
>> > for a small GHC patch that would enable my technique outlined above.
>> >
>> > ===== short story =====
>> >
>> > The motivation of dslAsTypeOf is to provide improved error messages
>> > when a and b are not equal.
>> >
>> > Unfortunately, the user will never see IndicativeErrorMessage. It
>> > appears that GHC does not attempt to solve C a b if a~b fails.
>> > That's understandable, since the solution of C a b almost certainly
>> > depends on the "value" of its arguments...
>> >
>> > Hence, the question at the top of this email.
>> >
>> > ===== long story =====
>> >
>> > A lot of the modern type-level programming capabilities can be put
>> > to great use in creating type systems for embedded domain specific
>> > languages. These type systems can enforce some impressive
>> properties.
>> >
>> > However, the error messages you get when one of those property is
>> > not satisfied can be pretty abysmal.
>> >
>> > In my particular case, I have a phantom type where the tag carries
>> > all the domain-specific information.
>> >
>> > > newtype U (tag :: [Info]) a = U a
>> >
>> > and I have an binary operation that requires the tag to be
>> > equivalent for all three types.
>> >
>> > > plus :: Num a => U tag a -> U tag a -> U tag a
>> > > plus (U x) (U y) = U $ x + y
>> >
>> > This effectively enforces the property I want for U values.
>> > Unfortunately, the error messages can seem dimwitted.
>> >
>> > > ill_typed = plus (U 1 :: U [Foo,Bar,Baz] Int) (U 2 :: U [Foo,Baz]
>> > Int)
>> >
>> > The `ill_typed` value gives an error message (in GHC 7.8) saying
>> >
>> > Bar : Baz : [] is not equal to Baz : []
>> >
>> > (It's worse in GHC 7.4. I don't have access to a 7.6 at the moment.)
>> >
>> > I'd much rather have it say that "Bar is missing from the first
>> > summand's list." And I can define a class that effectively conveys
>> > that information in a "domain-specific error message" which is
>> > actually a "no instance of <IndicativeClassName> tag1 tag2" message.
>> >
>> > > friendlier_plus :: (FriendlyEqCheck tag1 tag2 tag3,Num a) => U
>> > tag1 a -> U tag2 a -> U tag3 a
>> >
>> > The `friendlier_plus' function gives useful error messages if tag1,
>> > tag2, and tag3 are all fully monomorphic.
>> >
>> > However, it does not support inference:
>> >
>> > > zero :: Num a => U tag a
>> > > zero = U 0
>> > >
>> > > x = U 4 :: U [Foo,Baz] Int
>> > >
>> > > -- both of these are ill-typed :(
>> > > should_work1 = (friendlier_plus zero x) `asTypeOf` x -- tag1 is
>> > unconstrained
>> > > should_work2 = friendlier_plus x x -- tag3 is unconstrained
>> >
>> > Neither of those terms type-check, since FriendlyEqCheck can't
>> > determine if the unconstrained `tag' variable is equal to the other
>> > tags.
>> >
>> > So, can we get the best of both worlds?
>> >
>> > > best_plus ::
>> > > ( FriendlyEqCheck tag1 tag2 tag3
>> > , tag1 ~ tag2, tag2 ~ tag3, Num a) => U tag1 a -> U tag2 a -> U
>> > tag3 a
>> >
>> > No, unfortunately not. Now the `should_work*' functions type-check,
>> > but an ill-typed use of `best_plus' gives the same poor error
>> > message that `plus' would give.
>> >
>> > Hence, the question at the top of this email.
>> >
>> > ===== two ideas =====
>> >
>> > If my question at the top of this email cannot be answered in the
>> > affirmative, perhaps a small patch to GHC would make this sort of
>> > approach a viable lightweight workaround for improving
>> > domain-specific error messages.
>> >
>> > (I cannot estimate how difficult this would be to implement in the
>> > type-checker.)
>> >
>> > Two alternative ideas.
>> >
>> > 1) An "ALWAYS_ATTEMPT" PRAGMA that you can place on the class C so
>> > that it is attempted even if a related ~ constraint fails.
>> >
>> > 2) An OrElse constraint former, offering *very* constrained
>> > back-tracking.
>> >
>> > > possibleAsTypeOf :: ((a ~ b) `OrElse` C a b) => a -> b -> a
>> > > possibleAsTypeOf x _ = x
>> >
>> > Requirements: C must have no superclasses, no methods, and no
>> fundeps.
>> >
>> > Specification: If (a~b) fails and (C a b) is satisfiable, then the
>> > original inequality error message would be shown to the user. Else,
>> > C's error message is used.
>> >
>> > ===================================
>> >
>> > You made it to the bottom of the email! Thanks again.
>> >
>> >
>> >
>> >
>> > _______________________________________________
>> > 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/eb1ad35f/attachment.html>
More information about the ghc-devs
mailing list