Local evidence and type class instances
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
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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Fwd: Local evidence and type class instances
Forwarding to list.
-- Forwarded message --
From: Antoine Latter aslat...@gmail.com
Date: Sat, Oct 16, 2010 at 9:47 AM
Subject: Re: Local evidence and type class instances
To: Max Bolingbroke batterseapo...@hotmail.com
On Sat, Oct 16, 2010 at 7:11 AM, Max Bolingbroke
batterseapo...@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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Local evidence and type class instances
On Sat, Oct 16, 2010 at 7:11 AM, Max Bolingbroke batterseapo...@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 Along similar lines as my last post, would I be able to write the following type signature: myFunct :: Ord Int = Int - (...) and have it always use the local instance for Ord Int? Is this the type that the type checker would infer for my function? Antoine ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Local evidence and type class instances
HI Antoine, I didn't know UHC already had this - thanks for the pointer! It seems they have read about implicit configurations too, as the example they use is very similar to the paper. In fact, they also have another extension to the concept that I was intentionally avoiding mentioning - they ensure that the lexically most closely bound instance is used to satisfy a demand for a type class operation. This means that you can sensibly have local instances that overlap global ones. I'm not sure how I feel about this feature, though I certainly see the motivation. On 16 October 2010 15:47, Antoine Latter aslat...@gmail.com wrote: 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. That's the behaviour I had in mind. There is no doubt that local instances are a big complexity increase, but IMHO this behaviour is relatively easy to reason about as long as you know about the dictionary passing translation. Indeed, it's practically mandatory to use dictionary-passing to implement this behaviour. Local instances would probably never get added to a compiler (like JHC) that doesn't use that technique. RE your later point: Along similar lines as my last post, would I be able to write the following type signature: myFunct :: Ord Int = Int - (...) and have it always use the local instance for Ord Int? Is this the type that the type checker would infer for my function? To my mind, if you have that signature, then myFunct would use whatever Ord Int instance was available at the use site of myFunct (i.e. wherever it was mentioned syntactically). It is certainly interesting to note that adding a context like this might be useful if you were using local instances. Cheers, Max ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Local evidence and type class instances
On Sat, Oct 16, 2010 at 11:41 AM, Max Bolingbroke batterseapo...@hotmail.com wrote: On 16 October 2010 15:47, Antoine Latter aslat...@gmail.com wrote: 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. That's the behaviour I had in mind. There is no doubt that local instances are a big complexity increase, but IMHO this behaviour is relatively easy to reason about as long as you know about the dictionary passing translation. Indeed, it's practically mandatory to use dictionary-passing to implement this behaviour. Local instances would probably never get added to a compiler (like JHC) that doesn't use that technique. From the point of view of the down-stream engineer, I feel that first class modules with a module algebra like OCaml would be a lot less mysterious. Once a thing is locally scoped, it's nicer if I can name it and abstract over it in a concrete and reliable way. Keep in mind that I've never used OCaml's module system. Maybe that's just a lot harder to fit into GHC as it is today, though. But I feel like the problem you're solving has already been solved by first-class modules - type classes are for something else altogether. But maybe we need a better example to argue about :-) Antoine ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: un-used record wildcards
Hi Simon,
I've seen this issue with GHC 6.12.3 (and assumed it was by design).
It occurs with a slight modification of your example:
{-# LANGUAGE RecordWildCards #-}
module Test where
data T = MkT { f,g :: Int }
p x = let MkT{..} = x in f
This example warns about Defined but not used: `g' on the line
defining p. I've raised a GHC bug:
http://hackage.haskell.org/trac/ghc/ticket/4411 about this warning.
Thanks, Neil
Which version of GHC are you using? GHC 6.12 does not complain about unused
variables bound by ... Try this, which complains about y, but not g.
Simon
{-# LANGUAGE RecordWildCards #-}
module Test where
data T = MkT { f,g :: Int }
p (MkT { .. }) y = f
| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org
[mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Serge D. Mechveliani
| Sent: 14 October 2010 11:01
| To: Antoine Latter
| Cc: glasgow-haskell-users@haskell.org
| Subject: Re: un-used record wildcards
|
| On Wed, Oct 13, 2010 at 01:47:11PM -0500, Antoine Latter wrote:
| On Wed, Oct 13, 2010 at 1:02 PM, Serge D. Mechveliani mech...@botik.ru
| wrote:
| Dear GHC developers,
|
| I use the language extension of RecordWildcards, for example,
| f (Foo {foo1 = n, foo2 = m, ..}) = ...
|
| But the complier warns about un-used values of foo3, foo4,
| probably, due to the extension of
| Foo {foo1 = n, foo2 = m, foo3 = foo3, foo4 = foo4}.
|
| In such cases, these warnings look as unneeded.
| Is it possible to have an un-used binding warnings with exception for
| wildcards in records?
| If not, then has it sense to introduce an option?
|
|
| If you're not using foo3 and foo4, can you not put it the ellipsis?
| that won't cover every case (such as where you're using foo3 but not
| foo4).
|
| Antoine
|
|
| Indeed, thank you.
| It occurs that under RecordWildcards the compiler allows to skip some
| record fields in a pattern.
| ___
| Glasgow-haskell-users mailing list
| glasgow-haskell-us...@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
