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

19 Feb 2014

      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
mailto:nicolas.frisby@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@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs