Type Families and defaults
Hi! I see here: http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsStatus That defaults in type families are not yet implemented. But how far is this? And how far is overall implementation of this? There seems to be a lot of open bugs around that? Are type families meant to be used or is that still an experimental feature? For example, I have problems type checking the attached code (Test.hs). Is there a way to define a default function as I envisioned it? Or is this just broken code? ;-) It seems it is the later as also version with dependencies does not work (Test2.hs). Best regards Mitar
Mitar, and others Yes, I've spent most of the last month working on the new type checker, and unless there's a major hiccup it'll be in GHC 7.0. We'll produce a release candidate just before ICFP. However, as it happens both your tests compile with GHC 6.12, if you add ScopedTypeVariables. The trouble is that your type signatures like (IO n) are read as (forall n. IO n). It's a bit unfortunate that there isn't a more coherent warning about this. Suppose you write class C a where op :: a -> a op = .....(e :: a -> a).... Then the "a->a" signature means (in Haskell98) forall a. a->a. I suppose that I could add a warning that says more or less Warning: type signature implicitly quantifies over 'a', but if ScopedTypeVariables was on, type variable 'a' would be in scope here, so the type signature would not be quantified It's not trivial to add, but not really hard either. Has anyone else been bitten by this? Simon
On Mon, Sep 6, 2010 at 12:37 AM, Simon Peyton-Jones
Mitar, and others
Yes, I've spent most of the last month working on the new type checker, and unless there's a major hiccup it'll be in GHC 7.0. We'll produce a release candidate just before ICFP.
Ohh, how exciting, the big number is getting bigger! It's been a while since that happened.
Hi!
On Mon, Sep 6, 2010 at 9:37 AM, Simon Peyton-Jones
Yes, I've spent most of the last month working on the new type checker, and unless there's a major hiccup it'll be in GHC 7.0. We'll produce a release candidate just before ICFP.
That's great news! So if I understand those functions: mkLiveNeuron :: NeuronId -> LiveNeuron n getNeuronId :: LiveNeuron n -> NeuronId will not be necessary anymore with new type checked and improvements to type families?
However, as it happens both your tests compile with GHC 6.12, if you add ScopedTypeVariables. The trouble is that your type signatures like (IO n) are read as (forall n. IO n).
This trouble means that I can define something like the following? instance Neuron TestNeuron where data LiveNeuron TestNeuron = LiveTestNeuron NeuronId mkLiveNeuron nid = LiveTestNeuron nid getNeuronId (LiveTestNeuron nid) = nid live _ _ = return () attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO FooNeuron) dissolve (live nerve)) :: IO (LiveNeuron TestNeuron) Where obviously this makes little sense. (I made FooNeuron an instance of Neuron class but this is the only thing it enforced.) But it does not allow (as the TestNeuron instance): attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO FooNeuron) dissolve (live nerve)) :: IO (LiveNeuron FooNeuron) Which means that return type is checked well and n is from class definition. So n in "grow" function type is now locally scoped so it is independent from surrounding definitions of n. It is universally quantified and so it is some other type variable, even if it shares name with "n". Probably this is what you wrote, but I have to decipher your terminology a bit. ;-) But I do not understand how does then GHC pick correct definition in the case of default definition of "attach" function? If n is universally scoped and independent surrounding n, then it would be still ambiguous. Same as: attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO a) dissolve (live nerve)) :: IO (LiveNeuron n) But this later does not work. So n is connected to surrounding n. But then why it allows such instance definition as I mentioned above with FooNeuron and TestNeuron together?
It's not trivial to add, but not really hard either. Has anyone else been bitten by this?
It would be great if it would be added. Obviously I am for it. ;-) I think n should be scoped for the whole the class definition, everywhere, not just parameter and return values types. If somebody would define the same name for it for some local definition, GHC should make a "shadowing a variable" warning. Mitar
Mitar I'm afraid I didn't understand your questions well enough to answer them. But it'd be worth reading http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/other-type-extension... | > It's not trivial to add, but not really hard either. Has anyone else been | bitten by this? | | It would be great if it would be added. Obviously I am for it. ;-) | | I think n should be scoped for the whole the class definition, | everywhere, not just parameter and return values types. If somebody | would define the same name for it for some local definition, GHC | should make a "shadowing a variable" warning. I do rather agree. Let's see if others do. Simon
Hi!
I'm afraid I didn't understand your questions well enough to answer them.
My question is, why does this type check: instance Neuron TestNeuron where data LiveNeuron TestNeuron = LiveTestNeuron NeuronId mkLiveNeuron nid = LiveTestNeuron nid getNeuronId (LiveTestNeuron nid) = nid live _ _ = return () attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO FooNeuron) dissolve (live nerve)) :: IO (LiveNeuron TestNeuron) FooNeuron is obviously different to TestNeuron (but both are instances of Neuron class). Type signature is: attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: IO n) dissolve (live nerve)) :: IO (LiveNeuron n) This seems different to: attach nerve = ((liftM mkLiveNeuron) . forkIO $ bracket (grow :: forall n. IO n) dissolve (live nerve)) :: IO (LiveNeuron n) which does not type check. Maybe I am missing some basic understanding.
But it'd be worth reading http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/other-type-extension...
I had. Thanks. Mitar
| > I'm afraid I didn't understand your questions well enough to answer them.
|
| My question is, why does this type check:
It's hard for me to answer a question like that! To explain why something type checks I'd have to show every constraint and how it is solved.
I think you have something more specific in mind. Maybe you think "this should not typecheck". E.g. here's an expression (f x), and f has type Int ->
participants (3)
-
Evan Laforge -
Mitar -
Simon Peyton-Jones