Allowing Instances to Unify Types
Hi all, I've been hacking on GHC for a couple months now, experimenting with some different ideas I find interesting. One thing I'm trying to do is allow instance unifs (when there's an unambiguous choice, a question which is simplified in this case by there being only one), and force the required unification. Here's a simple example: {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} class Apply a b c | a b -> c where applyInst :: a -> b -> c instance (Monad m) => Apply (a -> m b) (m a) (m b) where applyInst = (=<<) apply :: (Monad m) => (a -> m b) -> (m a) -> (m b) apply = (=<<) ioStr :: IO String ioStr = return "foo" printStr :: String -> IO () printStr = print main = do print `apply` (return "foo") printStr `applyInst` ioStr print `applyInst` (return "bar") -- this fails With my code to use the unif instance enabled, I get Ambiguous type variable errors for "Show a" (from print) and "Monad m" (from return). My question is: in the case of apply (which isn't implemented by a class), how does the typechecker propagate "a ~ String" and "m ~ IO" to the predicates for print and return? If someone (such as myself) had sufficient time and energy to spend trying to achieve similar behavior for applyInst, where might he/I start? Thanks and Regards, -matt
You might want to wait a bit until the new type checker has made it
into mainline. The ideas behind the new type checker are explained in
the paper linked from here:
http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn
Here's an earlier thread about the new type checker:
http://comments.gmane.org/gmane.comp.lang.haskell.cafe/77413
On 23 July 2010 21:47, Matt Brown
Hi all, I've been hacking on GHC for a couple months now, experimenting with some different ideas I find interesting. One thing I'm trying to do is allow instance unifs (when there's an unambiguous choice, a question which is simplified in this case by there being only one), and force the required unification. Here's a simple example:
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} class Apply a b c | a b -> c where applyInst :: a -> b -> c
instance (Monad m) => Apply (a -> m b) (m a) (m b) where applyInst = (=<<)
apply :: (Monad m) => (a -> m b) -> (m a) -> (m b) apply = (=<<)
ioStr :: IO String ioStr = return "foo"
printStr :: String -> IO () printStr = print
main = do print `apply` (return "foo") printStr `applyInst` ioStr print `applyInst` (return "bar") -- this fails
With my code to use the unif instance enabled, I get Ambiguous type variable errors for "Show a" (from print) and "Monad m" (from return).
My question is: in the case of apply (which isn't implemented by a class), how does the typechecker propagate "a ~ String" and "m ~ IO" to the predicates for print and return? If someone (such as myself) had sufficient time and energy to spend trying to achieve similar behavior for applyInst, where might he/I start?
Thanks and Regards, -matt _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-- If it looks like a duck, and quacks like a duck, we have at least to consider the possibility that we have a small aquatic bird of the family Anatidae on our hands.
Matt I afraid I didn't understand your email well enough to offer a coherent response. For example I have no clue what "instance unifs" might mean. Nor do I understand what your program seeks to achieve. Thomas is right to say that the type checker is in upheaval at the moment. I'm actively working on it with Dimitrios (http://darcs.haskell.org/ghc-new-tc/ghc for the over-interested), but it'll be a month or two before it gets into HEAD. However the plan is to do so for the 6.14 release. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Matt Brown | Sent: 23 July 2010 21:47 | To: glasgow-haskell-users | Subject: Allowing Instances to Unify Types | | Hi all, | I've been hacking on GHC for a couple months now, experimenting with | some different ideas I find interesting. One thing I'm trying to do | is allow instance unifs (when there's an unambiguous choice, a | question which is simplified in this case by there being only one), | and force the required unification. Here's a simple example: | | {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, | FlexibleInstances, UndecidableInstances #-} | class Apply a b c | a b -> c where | applyInst :: a -> b -> c | | instance (Monad m) => Apply (a -> m b) (m a) (m b) where | applyInst = (=<<) | | apply :: (Monad m) => (a -> m b) -> (m a) -> (m b) | apply = (=<<) | | ioStr :: IO String | ioStr = return "foo" | | printStr :: String -> IO () | printStr = print | | main = do print `apply` (return "foo") | printStr `applyInst` ioStr | print `applyInst` (return "bar") -- this fails | | | With my code to use the unif instance enabled, I get Ambiguous type | variable errors for "Show a" (from print) and "Monad m" (from return). | | My question is: in the case of apply (which isn't implemented by a | class), how does the typechecker propagate "a ~ String" and "m ~ IO" | to the predicates for print and return? If someone (such as myself) | had sufficient time and energy to spend trying to achieve similar | behavior for applyInst, where might he/I start? | | Thanks and Regards, | -matt | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon and Thomas,
By instance unifs, I mean instances that do not match, but do "unify",
although I'm not entirely clear on what that means. My current
thinking is "could match, given some additional type information, such
as equality predicates". I refer to them as unifs, because that is
how they're labelled in the "lookupInst fail" message from
-ddump-tc-trace.
I've been toying with several ideas of dubious practicality, primarily
as a way to explore the inner workings of GHC (which has been great
fun btw). In this case, before TcSimplify.checkLoop exits, if irreds
is not null, reduceContext is run again with a flag that tells
lookupPred to accept an "instance unif", when a sensible choice can be
made (for example, when there is only one possible choice).
This is my limited understanding of the issue:
The expression: print `applyInst` (return "bar")
Contains three constraints: Show a, Monad m, and Apply (a -> IO ())
(m [Char]) (IO b)
Where the Show predicate is required by print, Monad by return, and
Apply by applyInst.
With my modifications, the lookup for the Apply predicate yields:
Apply ([Char] -> IO ()) (IO [Char]) (IO ())
Which implies two equality constraints (a ~ [Char], m ~ IO).
Knowing that, I'd like to be able to resolve (Show a, Monad m) as
(Show [Char], Monad IO). Put more simply, I'd like the applyInst
expression to typecheck as the apply expression does. Reading through
the OutsideIn paper over the weekend, I began to understand why it
isn't so simple. I'm looking forward to furthering my understanding,
and continuing my experiments with the new typechecker.
Thank you both for the informative responses,
-matt
On Mon, Jul 26, 2010 at 3:11 AM, Simon Peyton-Jones
Matt
I afraid I didn't understand your email well enough to offer a coherent response. For example I have no clue what "instance unifs" might mean. Nor do I understand what your program seeks to achieve.
Thomas is right to say that the type checker is in upheaval at the moment. I'm actively working on it with Dimitrios (http://darcs.haskell.org/ghc-new-tc/ghc for the over-interested), but it'll be a month or two before it gets into HEAD. However the plan is to do so for the 6.14 release.
Simon
| -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Matt Brown | Sent: 23 July 2010 21:47 | To: glasgow-haskell-users | Subject: Allowing Instances to Unify Types | | Hi all, | I've been hacking on GHC for a couple months now, experimenting with | some different ideas I find interesting. One thing I'm trying to do | is allow instance unifs (when there's an unambiguous choice, a | question which is simplified in this case by there being only one), | and force the required unification. Here's a simple example: | | {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, | FlexibleInstances, UndecidableInstances #-} | class Apply a b c | a b -> c where | applyInst :: a -> b -> c | | instance (Monad m) => Apply (a -> m b) (m a) (m b) where | applyInst = (=<<) | | apply :: (Monad m) => (a -> m b) -> (m a) -> (m b) | apply = (=<<) | | ioStr :: IO String | ioStr = return "foo" | | printStr :: String -> IO () | printStr = print | | main = do print `apply` (return "foo") | printStr `applyInst` ioStr | print `applyInst` (return "bar") -- this fails | | | With my code to use the unif instance enabled, I get Ambiguous type | variable errors for "Show a" (from print) and "Monad m" (from return). | | My question is: in the case of apply (which isn't implemented by a | class), how does the typechecker propagate "a ~ String" and "m ~ IO" | to the predicates for print and return? If someone (such as myself) | had sufficient time and energy to spend trying to achieve similar | behavior for applyInst, where might he/I start? | | Thanks and Regards, | -matt | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
| Knowing that, I'd like to be able to resolve (Show a, Monad m) as | (Show [Char], Monad IO). Put more simply, I'd like the applyInst | expression to typecheck as the apply expression does. Reading through | the OutsideIn paper over the weekend, I began to understand why it | isn't so simple. I'm looking forward to furthering my understanding, | and continuing my experiments with the new typechecker. OK. I'll keep the list posted about the new typechecker. Simon
participants (3)
-
Matt Brown -
Simon Peyton-Jones -
Thomas Schilling