[Haskell-cafe] DatatypeContexts / alternative

[Ben Franksen]

Am 24.02.21 um 11:17 schrieb Tom Ellis:
> It is a rare problem that gets simpler by the
> addition of type classes.

I disagree that this is a rare problem. It is a pervasive problem. It
crops up almost everywhere, at least that is my personal experience. And
I think Section 2 of the "Partial Type Constructors" paper shows that my
experience is not particularly unusual.

Cheers
Ben

>> ________________________________
>> From: Haskell-Cafe <haskell-cafe-bounces at haskell.org> on behalf of Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk>
>> Sent: 23 February 2021 19:27
>> To: haskell-cafe at haskell.org <haskell-cafe at haskell.org>
>> Subject: Re: [Haskell-cafe] DatatypeContexts / alternative
>>
>> This email was sent to you by someone outside the University.
>> You should only click on links or attachments if you are certain that the email is genuine and the content is safe.
>>
>> On Tue, Feb 23, 2021 at 06:37:06PM +0000, CASANOVA Juan wrote:
>>> Yes I realize that, but what I am expecting, I guess, is for the
>>> type checker to tell me (or anyone who tried to use it) that Foo (IO
>>> String) makes no sense, because Foo is always applied to something
>>> with Ord. That the very concept of the type Foo (IO String) itself
>>> does not type check.
>>>
>>> I realize the answer might be that this is impossible with current
>>> Haskell, but then a) Is there any fundamental reason why it is
>>> impossible
>>
>> Yes, there's a fundamental reason.  Neither you nor the compiler can
>> possibly know when invalid Foos (i.e. those whose parameter isn't Ord)
>> are constructed inside a function polymorphic in a  Functor . Let's
>> extend my example.
>>
>>     mapToUnit :: Functor f => f a -> f ()
>>     mapToUnit = fmap (const ()) . fmap (const getLine)
>>
>>     whatShouldItDo :: Foo ()
>>     whatShouldItDo = mapToUnit (Foo (Data.Map.singleton () ()))
>>
>> Do you agree that  whatShouldItDo  is well typed?  If not, why not?
>> If so, how should it behave when evaluated?  The implementation of
>>  mapToUnit , combined with your  Functor  instance says that  fromList
>> must be run on  [(getLine, getLine)] .  But this is impossible!
>>
>> Accepting that  whatShouldItDo  is well typed implies that you must
>> accept that your  Functor  instance for  Foo  cannot work.  (I don't
>> believe any instance can work if it is law-abiding but I don't know of
>> a proof.)
>>
>> There is a cottage industry of trying to work around this problem.
>> See, for example [1].  I have never seen a satisfactory solution.
>>
>> Based on your posts here you are frequently running into the limits of
>> type class based programming in Haskell.  If your purpose is practical
>> I strongly advise you to stay away from type classes for anything
>> non-trivial. Stick to the value level. Your life will be much
>> easier. If your purpose is research into type classes, or general
>> interest, then good luck and enjoy!
>>
>> Tom
>>
>>
>> [1] https://jeltsch.wordpress.com/2015/09/03/constrained-monads/
>>
>>
>>> ________________________________
>>> From: Haskell-Cafe <haskell-cafe-bounces at haskell.org> on behalf of Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk>
>>> Sent: 23 February 2021 18:29
>>> To: haskell-cafe at haskell.org <haskell-cafe at haskell.org>
>>> Subject: Re: [Haskell-cafe] DatatypeContexts / alternative
>>>
>>> This email was sent to you by someone outside the University.
>>> You should only click on links or attachments if you are certain that the email is genuine and the content is safe.
>>>
>>> On Tue, Feb 23, 2021 at 06:14:59PM +0000, CASANOVA Juan wrote:
>>>> module DatatypeContextsExample where
>>>>
>>>> import Data.Map
>>>> import Data.Bifunctor
>>>>
>>>> data Foo t = Foo (Map t t)
>>>>
>>>> instance Functor Foo where
>>>>     fmap f (Foo m) = Foo (fromList (fmap (bimap f f) (toList m)))
>>>>
>>>> This does not compile, because I am using toList and fromList, which
>>>> require (Ord t). But I cannot really have Foo be a functor in this
>>>> way without it. The thing is, every time I am going to use it, t is
>>>> actually going to be Ord. But how do I tell Haskell to have this
>>>> constraint?
>>>
>>> You say that every time you are going to use it t is actually going to
>>> be Ord, but how does the compiler know that when it comes to type
>>> check fmap?  After all, somewhere else you could write
>>>
>>>     fmap (const getLine) :: Foo t -> Foo (IO String)
>>>
>>> and  IO String  is certainly not Ord.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>