DatatypeContexts / alternative

CASANOVA Juan

23 Feb 2021 23 Feb '21

6:14 p.m.

Hello again, Haskell Cafe, Here again with another doubt on how am I supposed to. This one should be fairly easier, I believe. In short, I would like to have a functor type that can only be applied to certain type parameters. Why? Well, something like this: 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? DatatypeContexts seems to be the extension that allows this: data Ord t => Foo t = Foo (Map t t) But this has two issues. First, DatatypeContexts is deprecated. Second, more importantly, it still does not type check! It produces the exact same error, saying that Ord t could not be inferred. It should be inferred from the very fact that I am using the type Foo, but GHC does not seem to want to understand this. I could also try with GADTs: data Foo t where Foo :: Ord t => Map t t -> Foo t But this still gives the same error on the fmap definition, stating it cannot use Foo without Ord. But I am pattern-matching against it, shouldn't that be enough to know that (Ord t) is going to hold? I don't understand it. Is there anything simple I am missing? Any other simple way to achieve this? Any fundamental problem with what I am trying to do? Thanks as usual, Juan. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th' ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

Attachments:

attachment.html (text/html — 2.5 KB)

Show replies by date

CASANOVA Juan

23 Feb 23 Feb

6:21 p.m.

Reply to myself: I realized, with GADTs, it does assume Ord a, it's Ord b that fails. I can see how that cannot be derived from the context. Since Foo is only used for types with Ord, though, is there any way that I could let GHC know that this is going to be the case by definition. (So basically, in a way that would make fmap not typecheck on Foo when trying to use a function (a -> b) where Ord b does not hold) Sorry I did not realize this earlier. ________________________________ From: Haskell-Cafe on behalf of CASANOVA Juan Sent: 23 February 2021 18:14 To: haskell-cafe@haskell.org Subject: [Haskell-cafe] DatatypeContexts / alternative Hello again, Haskell Cafe, Here again with another doubt on how am I supposed to. This one should be fairly easier, I believe. In short, I would like to have a functor type that can only be applied to certain type parameters. Why? Well, something like this: 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? DatatypeContexts seems to be the extension that allows this: data Ord t => Foo t = Foo (Map t t) But this has two issues. First, DatatypeContexts is deprecated. Second, more importantly, it still does not type check! It produces the exact same error, saying that Ord t could not be inferred. It should be inferred from the very fact that I am using the type Foo, but GHC does not seem to want to understand this. I could also try with GADTs: data Foo t where Foo :: Ord t => Map t t -> Foo t But this still gives the same error on the fmap definition, stating it cannot use Foo without Ord. But I am pattern-matching against it, shouldn't that be enough to know that (Ord t) is going to hold? I don't understand it. Is there anything simple I am missing? Any other simple way to achieve this? Any fundamental problem with what I am trying to do? Thanks as usual, Juan. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

Viktor Dukhovni

6:33 p.m.

On Tue, Feb 23, 2021 at 06:21:23PM +0000, CASANOVA Juan wrote:

...

I realized, with GADTs, it does assume Ord a, it's Ord b that fails. I can see how that cannot be derived from the context. Since Foo is only used for types with Ord, though, is there any way that I could let GHC know that this is going to be the case by definition.

This is NOT a GHC issue, this is a library issue. To be a "Functor", a data structure MUST accept values of any type. This is essential in Monads, where we, e.g., expect "return" to be able to return any value. It seems you want to work with the endo-functors of a sub-category of "Hask", so perhaps: https://hackage.haskell.org/package/constrained-category-0.1.0.0/docs/Data-F... but then of course, you have to limit yourself to functions that work within that category, so the standard "fmap" is not available, standard Monads are not available, ... -- Viktor.

Tom Ellis

6:29 p.m.

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?

CASANOVA Juan

6:37 p.m.

Tom, 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, like it would never be possible to do this, or is it just a feature that is not clear how to implement in GHC? and b) The basic problem that I have: Implementing an fmap for something like Foo. Can I really just not do it in any way or shape, with any form of workaround? So far what I have been doing with situation similar to this is to just create the function fmap_foo that does what fmap does, with the proper constraints. But this is not enough when later on I want to use some other function that requires Foo to actually implement Functor. It would basically mean I have to re-implement all the structure while adding all the additional "Ord" constraints. Thanks, Juan. ________________________________ 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. Tom _______________________________________________ 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. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th' ann an Oilthigh Dh?n ?ideann, cl?raichte an Alba, ?ireamh cl?raidh SC005336.

Richard Eisenberg

7:07 p.m.

Hi café, You might be interested in my recent paper on exactly this problem: how to make DatatypeContexts actually work the way you want: https://richarde.dev/papers/2020/partialdata/partialdata.pdf https://richarde.dev/papers/2020/partialdata/partialdata.pdf. Sections 1-3 and 6 onwards should be approachable with only a Haskell background (but not, say, type theory). (Section 4 gives details about the design, but these details are broadly inferrable from the other sections. Section 5 is a proof that the idea is sound; you can just take this on faith.) There are, sadly, no plans to implement this paper, because the interactions with other GHC features means that implementing this would require dependent types. But perhaps with dependent types, we'll choose to go in this direction. In my role as a GHC Steering Committee member, I'm leery of proposals which would bring GHC further from the ideal expressed in this paper. Richard

...

On Feb 23, 2021, at 1:37 PM, CASANOVA Juan wrote:

Tom,

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, like it would never be possible to do this, or is it just a feature that is not clear how to implement in GHC? and b) The basic problem that I have: Implementing an fmap for something like Foo. Can I really just not do it in any way or shape, with any form of workaround?

So far what I have been doing with situation similar to this is to just create the function fmap_foo that does what fmap does, with the proper constraints. But this is not enough when later on I want to use some other function that requires Foo to actually implement Functor. It would basically mean I have to re-implement all the structure while adding all the additional "Ord" constraints.

Thanks, Juan.

From: Haskell-Cafe mailto:haskell-cafe-bounces@haskell.org> on behalf of Tom Ellis mailto:tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> Sent: 23 February 2021 18:29 To: haskell-cafe@haskell.org mailto:haskell-cafe@haskell.org mailto: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.

Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Ben Franksen

28 Feb 28 Feb

8:25 a.m.

Am 23.02.21 um 20:07 schrieb Richard Eisenberg:

...

You might be interested in my recent paper on exactly this problem: how to make DatatypeContexts actually work the way you want: https://richarde.dev/papers/2020/partialdata/partialdata.pdf https://richarde.dev/papers/2020/partialdata/partialdata.pdf. Sections 1-3 and 6 onwards should be approachable with only a Haskell background (but not, say, type theory). (Section 4 gives details about the design, but these details are broadly inferrable from the other sections. Section 5 is a proof that the idea is sound; you can just take this on faith.)

Richard, this is absolutely fantastic! I have just read as far as the listed contributions and I think this exactly what we need.

...

There are, sadly, no plans to implement this paper, because the interactions with other GHC features means that implementing this would require dependent types.

What are these other GHC features? Does the paper explain this? Otherwise where can I read more about it? Cheers Ben

...

...
On Feb 23, 2021, at 1:37 PM, CASANOVA Juan wrote:

Tom,

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, like it would never be possible to do this, or is it just a feature that is not clear how to implement in GHC? and b) The basic problem that I have: Implementing an fmap for something like Foo. Can I really just not do it in any way or shape, with any form of workaround?

So far what I have been doing with situation similar to this is to just create the function fmap_foo that does what fmap does, with the proper constraints. But this is not enough when later on I want to use some other function that requires Foo to actually implement Functor. It would basically mean I have to re-implement all the structure while adding all the additional "Ord" constraints.

Thanks, Juan.

From: Haskell-Cafe mailto:haskell-cafe-bounces@haskell.org> on behalf of Tom Ellis mailto:tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> Sent: 23 February 2021 18:29 To: haskell-cafe@haskell.org mailto:haskell-cafe@haskell.org mailto: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.

Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ 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.

Richard Eisenberg

7 p.m.

...

On Feb 28, 2021, at 3:25 AM, Ben Franksen wrote:

What are these other GHC features? Does the paper explain this? Otherwise where can I read more about it?

I think it was data families. But, perhaps more troublesome is the fact that the paper assumes a dependently-typed internal language. Maybe it's possible to do this without dependent types in the internal language, but I'm not sure how to begin to think about that problem. I was about to write that it might be helpful to have a GHC proposal to implement this paper, which would depend on (and provide further motivation for) having dependent types... but I'm not actually sure that would be productive at this point. I have spent some time thinking about how to clear my decks to make more time for implementation work, and I expect to prioritize this more going forward. Richard

Ben Franksen

1 Mar 1 Mar

11:36 a.m.

Am 28.02.21 um 20:00 schrieb Richard Eisenberg:

...

...
On Feb 28, 2021, at 3:25 AM, Ben Franksen wrote:

What are these other GHC features? Does the paper explain this? Otherwise where can I read more about it?

I think it was data families. But, perhaps more troublesome is the fact that the paper assumes a dependently-typed internal language. Maybe it's possible to do this without dependent types in the internal language, but I'm not sure how to begin to think about that problem.

I see. So this cannot be expressed in, say, System Fc? I wonder... is it possible to pinpoint where System Fc is not sufficiently expressive? Perhaps trying to do so exposes a way to extend System Fc that allows to implement this scheme, ideally as step towards a dependently typed IL w/o going the full way. Sorry if these questions are completely naive! I am not versed enough in type theory to full grasp the formulas in these papers in all detail.

...

I was about to write that it might be helpful to have a GHC proposal to implement this paper, which would depend on (and provide further motivation for) having dependent types... but I'm not actually sure that would be productive at this point.

Yes, this seems to be of relevance only in the very long run. Cheers Ben

Tom Ellis

23 Feb 23 Feb

7:27 p.m.

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.

CASANOVA Juan

8:09 p.m.

Thanks Tom, After the last email I sent, I was left thinking that the way in which this could be a problem was some generic Functor function that had intermediate values that could violate the constraints, but such that it's type signature respected it, but I didn't think much else on it. I think your example is exactly this: you use the getLine fmap inside the function, which is fine for a general Functor, but produces a temporary no-Ord functor, while the overall function preserves the signature. And yeah, the only possible way to go around this would be to actually have additional "notes" on the signature of functions which said what it internally needed, which not only is horrendous but I believe crashes strongly against a lot of other things we do in Haskell (or any similar language for that matter) So, yeah, I understand the issue. To respond to your last comment. First, I realize this is not what you are saying, but please someone do let me know if at some point my posts feel excessive or out of place. I have a strong issue with both often not being able to tell the social context very well and also being very insecure about making a fool out of myself for that reason. Second, my situation is practical (my research is not on programming languages), but I cannot deny I like an elegant solution like most other people here probably do, so I often go a bit further than strictly necessary out of curiosity. This is not the case in this instance, though. This is still giving me problems and I still haven't found a satisfactory workaround for my particular problem, no matter how "dirty" it would be. I think I'll figure it out eventually, though. It seems to be just a matter of instantiating enough type variables to exactly what I want to use them for. I do see your suggestion, one that I had considered myself; but it's more useful coming from someone who seems to know what they're doing better than me, so that if I end up deciding to avoid type classes for certain complex things I am more secure it's not just me being dumb, but rather that there be dragons that I don't want to fight. However, a practical issue with avoiding type classes tends to be that function signatures tend to become larger, larger and larger, making the code very very cluttered. So I think that's where the art comes, in finding the balance between those two things. A lot of my complex issues come from a sort-of obsession with making code as modular as possible. This is a long topic and I know it's not a "solvable" problem, but I try to push things as far as I can in that regard (within reason, I try). Thanks again, this does respond everything I doubted about this particular issue. Juan. ________________________________ 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

...

________________________________ 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. The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th' ann an Oilthigh Dh?n ?ideann, cl?raichte an Alba, ?ireamh cl?raidh SC005336.

Tom Ellis

24 Feb 24 Feb

10:17 a.m.

On Tue, Feb 23, 2021 at 08:09:21PM +0000, CASANOVA Juan wrote:

...

please someone do let me know if at some point my posts feel excessive or out of place.

I think your questions are perfectly reasonable for this list and many people here, including me, will enjoy thinking about them and answering them. My suggestion is purely to point out that, in practical terms, there are probably much more direct and simple routes to achieving your goal. It is a rare problem that gets simpler by the addition of type classes. That being said, there's also a lot of value in deeply exploring different approaches even if they don't turn out to be practical in the end. Tom

...

________________________________ 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.

Ben Franksen

28 Feb 28 Feb

8:38 a.m.

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.

Tom Ellis

8:52 a.m.

On Sun, Feb 28, 2021 at 09:38:17AM +0100, Ben Franksen wrote:

...

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.

I think I must have use language that was unnecessarily confusing. My meaning was "Only rarely is a problem simplified by the addition of typeclasses" Tom

Ben Franksen

11:40 a.m.

Am 28.02.21 um 09:52 schrieb Tom Ellis:

...

On Sun, Feb 28, 2021 at 09:38:17AM +0100, Ben Franksen wrote:

...
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.

I think I must have use language that was unnecessarily confusing. My meaning was

"Only rarely is a problem simplified by the addition of typeclasses"

Oops. No objection to that! Cheers Ben

1588

Age (days ago)

1594

Last active (days ago)

List overview

Download

14 comments

5 participants

participants (5)

Ben Franksen
CASANOVA Juan
Richard Eisenberg
Tom Ellis
Viktor Dukhovni