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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140130/fb52363e/attachment.html>

Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
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>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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140130/b2d31614/attachment-0001.html>

Reply | Threaded
Open this post in threaded view
|

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

Adam Gundry-2
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/

Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
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

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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140210/89128fbc/attachment-0001.html>

Reply | Threaded
Open this post in threaded view
|

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

José Pedro Magalhães
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>

Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
On Tue, Feb 11, 2014 at 3:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:

> On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <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 "."
>        )
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140211/94de443b/attachment.html>

Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
Are we reaching the point where a wiki page and perhaps (soon) a Trac
ticket would be appropriate?


On Tue, Feb 11, 2014 at 10:10 AM, Nicolas Frisby
<nicolas.frisby at gmail.com>wrote:

> On Tue, Feb 11, 2014 at 3:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl>wrote:
>
>> On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <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 "."
> >        )
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140211/0d73f780/attachment.html>

Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
In reply to this post by Nicolas Frisby
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> wrote:

> On Tue, Feb 11, 2014 at 3:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
> On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <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
> 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/193c764a/attachment-0001.html>

Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
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.
On Feb 11, 2014 12:15 PM, "Richard Eisenberg" <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>
> wrote:
>
> On Tue, Feb 11, 2014 at 3:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl>wrote:
>
>> On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <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
> 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/c37368d2/attachment.html>

Reply | Threaded
Open this post in threaded view
|

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

Adam Gundry-2
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/

Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
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>

Reply | Threaded
Open this post in threaded view
|

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

Jonathan Paugh
In reply to this post by Adam Gundry-2
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
>>
>
>



Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
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