Re: Local types and instances

[Matthew Farkas-Dyck]

On 4/29/18, Edward Kmett  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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

Re: Local types and instances

[Edward Kmett]

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  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
> Haskell-prime@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

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
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime