[Haskell-cafe] DatatypeContexts / alternative

[Tom Ellis]

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.