[Haskell-cafe] DatatypeContexts / alternative

[Ben Franksen]

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 <Juan.Casanova at ed.ac.uk>
>> 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 <haskell-cafe-bounces at haskell.org
>> <mailto:haskell-cafe-bounces at haskell.org>> on behalf of Tom Ellis
>> <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk
>> <mailto:tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk>> Sent: 23
>> February 2021 18:29 To: haskell-cafe at haskell.org
>> <mailto:haskell-cafe at haskell.org> <haskell-cafe at haskell.org
>> <mailto: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.
>> 
>> 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.
>