workaround to get both domain-specific errors and also multi-modal type inference?

[Richard Eisenberg]

Though I favor the approach Adam wrote about (he and I discussed it before his post), I think these are very valid concerns, and would have to be taken into account in the design of any further work in this area.

One observation I would make now is that none of this proposal, as far as I can tell, would change run-time behavior of any program. This proposal concerns only generation of error messages -- correct programs would not notice the feature. Now, you're right to be concerned about the possibility of DSL-specific error messages outside of the DSL! But, my hunch is that it would fairly well-managed, because the DSL-specific messages would be tied to the use of DSL constructs, which would not appear outside of DSL code. That defense is very hand-wavy, and we would want to be more sure that we don't "leak", but I'm not terribly worried about it right now.

I will say that, for better or worse, GHC already has constructs that can affect runtime behavior unexpectedly, particularly {#- RULES #-}.

Richard

On Feb 19, 2014, at 8:25 AM, Jonathan Paugh wrote:

> On 02/07/2014 03:05 PM, Adam Gundry 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
> 
> Strictly from an API-design point of view, I think having __special__
> functions that influence the compiler[0] is a __really__ __bad__ idea.
> (Think of __Python__, where even basic language constructs can be
> ruthlessly mangled.) How would these special functions behave? Using
> type classes *might* make that okay, but what to __avoid__ (IMO) is
> having the compiler treat objects/modules/etc differently based on
> whether certain values are defined. It leads to in-cohesiveness, and
> mal-comprehension.
> 
> Would you really want a module/function, etc to behave differently based
> on whether some value were in scope when it was defined? Even for
> something as benign as error messages? How would you limit the scope of
> your changes? Would a type class really cut it, especially with the way
> instances are propagated?
> 
> This kind of thinking might make more sense if modules were somehow
> first-class objects, with a reasonable interface for toying with them
> generally. (No comment on whether *that's* a good idea.)
> 
>>    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.
> 
> I'm not a type-foo master, but wouldn't it be hard to restrict the
> effects of a type class-based solution to strictly your own code?
> Wouldn't it be easy to have multiple, overlapping instances in various
> places? How would we keep from seeing DSL-specific error messages out of
> context?
> 
> Like I said, I can't talk about this from the perspective of an
> implementor, or even a library-designer who might use this feature; I'm
> merely a library-user who'd have to deal with it.
> 
> [0] I exclude TH, which has a well-defined separation from normal code.
> Perhaps one could cook up a good, well-defined API for this, too, but I
> have doubts...
> 
> Regards,
> Jonathan Paugh
> 
>> 
>> 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
>>> 
>> 
>> 
> 
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs