Local types and instances

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Local types and instances

M Farkas-Dyck
Idea: Allow local type and instance declarations, i.e. in `let` or `where` clause.

Primary motivation: defining `ordNubBy` and such, i.e. functions which take an effective class dictionary

In Haskell now, we can readily write `ordNubOn :: Ord b => (a -> b) -> [a] -> [a]` in terms of `Set` [0], but not `ordNubBy :: (a -> a -> Ordering) -> [a] -> [a]`, as `Set` requires an `Ord` instance. This is for good reason — incoherence would destroy the guaranties of `Set` — but in the case of `ordNubBy`, the `Set` would never escape, so it's fine. I needed `ordNubBy` in a past job, so we actually copied much of the `Set` code and modified it to take an `(a -> a -> Ordering)` rather than have an `Ord` constraint, which works but is unfortunate. This proposal would allow the following:

```
ordNubBy :: (a -> a -> Ordering) -> [a] -> [a]
ordNubBy f = let newtype T = T { unT :: a }
                  instance Ord T where compare = f
              in fmap unT . ordNub . fmap T
```

Secondary motivation: defining local utility types in general

Note: The primary motivation is a subcase of this, with local instances defined in terms of local arguments.

It is sometimes convenient or necessary to define a utility type which is only used in the scope of a single term. It would be nice to be able to define this in a `let` or `where` clause rather than at top level, for the same reason it is nice to be able to define helper functions there.

Semantics:
My thought is the local type is unique to each use of the term it is defined in, to not cause incoherence. I believe the implementation should be feasible as typeclass constraints are lowered to dictionary arguments anyhow. But i am neither a type theorist nor an expert in GHC so please point out any flaws in my idea.

I'm also thinking the type of the term where the local type is defined is not allowed to contain the local type. I'm not sure what the soundness implications of allowing this (unique) type to escape would be, but it seems like it might lead to confusing error messages when types which seem to have the same name can't be unified, and generally trips my informal mental footgun alarm.

Thoughts?

[0] https://gist.github.com/strake/333dfd697a1ade4fea69e6c36536fc16
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Local types and instances

Edward Kmett-2
This isn't sound.

You lose the global uniqueness of instance resolution, which is a key part of how libraries like Data.Set and Data.Map move the constraints from being carried around in the Set to the actual use sites. With "local" instances it is very easy to construct such a map in one local context and use it in another with a different instance.

This issue is mentioned at the end the very first paper in which typeclasses were introduced as losing principal typings when the definitions aren't top level.

The reify/reflect approach from the reflection package allows this sort of thing without lose of principal typing through generativity. This lets you write instances that depend on values in scope by reifying the value as a fresh type that has an associated instance that can be used to get your value back. The type variable generated is always "fresh" and doesn't violate any open world assumptions or have any concerns like the above Set/Map situation.

-Edward

> On Apr 29, 2018, at 6:28 PM, M Farkas-Dyck <[hidden email]> wrote:
>
> Idea: Allow local type and instance declarations, i.e. in `let` or `where` clause.
>
> Primary motivation: defining `ordNubBy` and such, i.e. functions which take an effective class dictionary
>
> In Haskell now, we can readily write `ordNubOn :: Ord b => (a -> b) -> [a] -> [a]` in terms of `Set` [0], but not `ordNubBy :: (a -> a -> Ordering) -> [a] -> [a]`, as `Set` requires an `Ord` instance. This is for good reason — incoherence would destroy the guaranties of `Set` — but in the case of `ordNubBy`, the `Set` would never escape, so it's fine. I needed `ordNubBy` in a past job, so we actually copied much of the `Set` code and modified it to take an `(a -> a -> Ordering)` rather than have an `Ord` constraint, which works but is unfortunate. This proposal would allow the following:
>
> ```
> ordNubBy :: (a -> a -> Ordering) -> [a] -> [a]
> ordNubBy f = let newtype T = T { unT :: a }
>                 instance Ord T where compare = f
>             in fmap unT . ordNub . fmap T
> ```
>
> Secondary motivation: defining local utility types in general
>
> Note: The primary motivation is a subcase of this, with local instances defined in terms of local arguments.
>
> It is sometimes convenient or necessary to define a utility type which is only used in the scope of a single term. It would be nice to be able to define this in a `let` or `where` clause rather than at top level, for the same reason it is nice to be able to define helper functions there.
>
> Semantics:
> My thought is the local type is unique to each use of the term it is defined in, to not cause incoherence. I believe the implementation should be feasible as typeclass constraints are lowered to dictionary arguments anyhow. But i am neither a type theorist nor an expert in GHC so please point out any flaws in my idea.
>
> I'm also thinking the type of the term where the local type is defined is not allowed to contain the local type. I'm not sure what the soundness implications of allowing this (unique) type to escape would be, but it seems like it might lead to confusing error messages when types which seem to have the same name can't be unified, and generally trips my informal mental footgun alarm.
>
> Thoughts?
>
> [0] https://gist.github.com/strake/333dfd697a1ade4fea69e6c36536fc16
> _______________________________________________
> Haskell-prime mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Local types and instances

M Farkas-Dyck
On 4/29/18, Edward Kmett <[hidden email]> wrote:
> This isn't sound.
>
> You lose the global uniqueness of instance resolution, which is a key part
> of how libraries like Data.Set and Data.Map move the constraints from being
> carried around in the Set to the actual use sites. With "local" instances it
> is very easy to construct such a map in one local context and use it in
> another with a different instance.

Ah, i forgot to say explicitly: local instances of types declared at
greater scope are not allowed. Is it unsound nonetheless?
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Local types and instances

Gershom Bazerman
Given the open world assumption, how do you know a priori if a type is declared at greater scope?

(Note: one answer here is that you can refuse to link in such a contradictory instance, so instead of an ‘open world’ you move to a ‘coherent world’ where you have to discharge a global coherence constraint check at compile time — I never fully fleshed this out, but I think it might open a number of interesting possibilities).

(Also — I just realized this is in the wrong location — the haskell-prime list. Proposals like this that do not exist yet in any compiler tend to be out of scope for the prime process, such as it exists. It would be better to produce a sketch and ask for feedback in a different venue — perhaps glasgow-haskell-users, and if you reach a point where you have a full spec then you can submit it through the ghc proposals process.)

-g


On April 29, 2018 at 7:37:30 PM, Matthew Farkas-Dyck ([hidden email]) wrote:

On 4/29/18, Edward Kmett <[hidden email]> wrote:
> This isn't sound.
>
> You lose the global uniqueness of instance resolution, which is a key part
> of how libraries like Data.Set and Data.Map move the constraints from being
> carried around in the Set to the actual use sites. With "local" instances it
> is very easy to construct such a map in one local context and use it in
> another with a different instance.

Ah, i forgot to say explicitly: local instances of types declared at
greater scope are not allowed. Is it unsound nonetheless?
_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Local types and instances

Edward Kmett-2
In reply to this post by M Farkas-Dyck
If your instances are allowed to depend on values that are in scope in your nested context then the choice of those values is effectively part of the name of the data type. Otherwise I can package one of those 'local' data type definitions up, pass it out into another context that brings it back under the `where` clause that defined the local data type with a different value. So, yes, unless you're willing to figure out how to somehow decide the equality of arbitrary values and functions. If you try to say you can't write that sort of scenario by using some sort of magical generative trick that says each invocation of the function that got you down to that data type gives you an entirely 'fresh' type, I suspect you'll run into subtle problems with unification / type checking. I'd love to be wrong, but my expectation is that all of these paths fail.

In any event, Gershom is right, this is the wrong forum for this discussion.

-Edward


On Sun, Apr 29, 2018 at 7:37 PM, Matthew Farkas-Dyck <[hidden email]> wrote:
On 4/29/18, Edward Kmett <[hidden email]> wrote:
> This isn't sound.
>
> You lose the global uniqueness of instance resolution, which is a key part
> of how libraries like Data.Set and Data.Map move the constraints from being
> carried around in the Set to the actual use sites. With "local" instances it
> is very easy to construct such a map in one local context and use it in
> another with a different instance.

Ah, i forgot to say explicitly: local instances of types declared at
greater scope are not allowed. Is it unsound nonetheless?


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime