Re: [Haskell-cafe] DatatypeContexts / alternative

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 on behalf of Tom Ellis Sent: 23 February 2021 19:27 To: haskell-cafe@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 on behalf of Tom Ellis Sent: 23 February 2021 18:29 To: haskell-cafe@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.