Fwd: Local evidence and type class instances

[Antoine Latter]

Forwarding to list.


---------- Forwarded message ----------
From: Antoine Latter <aslatter at gmail.com>
Date: Sat, Oct 16, 2010 at 9:47 AM
Subject: Re: Local evidence and type class instances
To: Max Bolingbroke <batterseapower at hotmail.com>


On Sat, Oct 16, 2010 at 7:11 AM, Max Bolingbroke
<batterseapower at hotmail.com> wrote:
> Hi GHC users,
>
> Now that the Glorious New type checker can handle local evidence
> seamlessly, is it a big implementation burden to extend it to deal
> with local *type class instances* in addition to local *equality
> constraints*?
>
> For example, you could write this:
>
> """
> f :: Bool
> f = id < id
>  where
>   instance Ord (a -> b) where
>     _ `compare` _ = LT
> """

I think UHC has something like that:
http://www.cs.uu.nl/wiki/bin/view/Ehc/UhcUserDocumentation#3_8_Local_instances

One thing that worries me is that the local instance only applies to
type-expressions that consume constraints - if the constraint was
satisfied before the local constraint was introduced then the local
constraint would not apply.

Am I making sense? I don't have much of a background in type-theory,
so I may not be using the correct language, but I'm having trouble
seeing how it wouldn't be confusing.

What I'm thinking is that the following two functions would have
different effect:

f n = Set.insert n

and:

f' (n::Int) = Set.insert n

When called like so:

updateSet (n::Int) s =
  let n' = someComputation n s
  in f n' s
 where instance Ord s ...

Substituting f for f' in this example will change the meaning of the
operation significantly, which is, in my mind, hard to explain and
reason about.

Type-classes are engineered to be global in scope. It's nice that from
a GHC type-checking perspective they need not be, but changing them to
be non-global is also an engineering and design problem.

Antoine

>
> Not only would this prevent instances from "leaking" into all
> importing modules, but you could refer to *lexically scoped variables*
> in the type class instance. This would let programmers implement e.g.
> implicit configurations in the style of Kieslyov and Shan
> (http://okmij.org/ftp/Haskell/types.html#Prepose) without any mad
> hackery to tunnel pointers through the type system.
>
> Of course, it could lead to problems. For example:
>
> """
> newtype MyInt = MyInt { unMyInt :: Int }
>
> f :: [Int] -> S.Set Int
> f xs = S.map unMyInt $ S.toList (map MyInt xs)
>  where
>   instance Ord MyInt where
>     x `compare` y = unMyInt x `compare` unMyInt y
>
> g :: [Int] -> S.Set Int
> g xs = S.map unMyInt $ S.toList (map MyInt xs)
>  where
>   instance Ord MyInt where
>     x `compare` y = unMyInt y `compare` unMyInt x
>
> main = do
>  let s1 = f [1, 2]
>     s2 = g [1, 2]
>  print $ s1 == s2  -- prints False!
>  print $ S.toList s1 == s2  -- prints True!
> """
>
> I don't think this is a big problem. It would be up to the users of
> this extension to do the Right Thing.
>
> As Kieslyov and Shan point out, this extension also kills the
> principal types property - but so do GADTs. Just add more type
> signatures!
>
> Are there big theoretical problems with this extension, or is it just
> a lack of engineering effort that has prevented its implementation?
>
> Max
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>