Hunting for ghci manual input vs. file input differences again
Hi, I've been working on a kind of constrained version of Data.Dynamic: data Dynamic (c :: * -> Constraint) where Dynamic :: (Typeable a, c a) => a -> Dynamic c The idea is that Data.Dynamic gives up all compile time type information. In this variant I can at least keep a bit of the information around that I have. (In fact I can even "lift" a type into a constraint, thereby keeping /all/ information.) Most of my functions are nailed down, including mappings and traversals. But one group of functions eludes me: functions to change only the constraint, while keeping the value. Here is one of my goal types: castDynamic :: ( Typeable a, c a, d a ) => Dynamic c -> Dynamic d I'm pretty sure I'll have to sprinkle in a Proxy a, but so be it. I've thrown all typing tricks at this function that I know of, from unsafeCoerce over case-of instead of pattern matching, to ScopedTypeVariables. But I couldn't convince ghci to accept my code. So I tried something simpler. castDynamic' :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c) Here's where it gets funny: I can implement this function in ghci interactively just fine. >>> :t \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c) But when I enter the exact same code in a file and load it, ghci balks at me because a is too ambiguous. Again, I've tried if it's the monomorphism restriction, or if I need to sprinkle in more (scoped) signatures or explicit forall's etc… nothing helped. What is the difference here? Am I missing an extension? Am I doing something I shouldn't and the interactive mode is just doing me a favor? There was a discussion on this list less than a month ago where it was mentioned that ghci handles polymorphic types differently depending on the source of the code. Is there some documentation on these differences? Any help would be appreciated. Cheers, MarLinn
The type `a` only appears in the constraints, not the signature, so GHC has
no way of figuring out what it's supposed to be. Furthermore, the type `a`
in your signature is *not* the type `a` that's in the GADT -- that's a
totally distinct type. I don't think you'll be able to unify the those two
types.
You can use a `Proxy` argument to explicitly signal to GHC what type it
should be, or TypeApplications, but I don't think either of those will help
with implementing this.
You may also find
http://haddock.stackage.org/lts-5.1/constraints-0.8/Data-Constraint.html
interesting.
Matt Parsons
On Thu, May 4, 2017 at 9:55 PM, MarLinn
Hi,
I've been working on a kind of constrained version of Data.Dynamic:
data Dynamic (c :: * -> Constraint) where Dynamic :: (Typeable a, c a) => a -> Dynamic c
The idea is that Data.Dynamic gives up all compile time type information. In this variant I can at least keep a bit of the information around that I have. (In fact I can even "lift" a type into a constraint, thereby keeping *all* information.) Most of my functions are nailed down, including mappings and traversals. But one group of functions eludes me: functions to change only the constraint, while keeping the value. Here is one of my goal types:
castDynamic :: ( Typeable a, c a, d a ) => Dynamic c -> Dynamic d
I'm pretty sure I'll have to sprinkle in a Proxy a, but so be it. I've thrown all typing tricks at this function that I know of, from unsafeCoerce over case-of instead of pattern matching, to ScopedTypeVariables. But I couldn't convince ghci to accept my code. So I tried something simpler.
castDynamic' :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)
Here's where it gets funny: I can implement this function in ghci interactively just fine.
:t \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)
But when I enter the exact same code in a file and load it, ghci balks at me because a is too ambiguous. Again, I've tried if it's the monomorphism restriction, or if I need to sprinkle in more (scoped) signatures or explicit forall's etc… nothing helped.
What is the difference here? Am I missing an extension? Am I doing something I shouldn't and the interactive mode is just doing me a favor? There was a discussion on this list less than a month ago where it was mentioned that ghci handles polymorphic types differently depending on the source of the code. Is there some documentation on these differences? Any help would be appreciated.
Cheers, MarLinn
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
You can use a `Proxy` argument to explicitly signal to GHC what type it should be, or TypeApplications, but I don't think either of those will help with implementing this.
I guess you're right. It seems my examples where only working because somewhere along the line types where defaulted to () – throwing away any information I did have. I suppose what I would actually need for the elusive cast is something like a (forall a . c a :=> d a). I found some interesting bits in Data.Constraint.Forall to pursue in that direction, but I'm far from understanding how to use them. Anyway, thanks for the help. MarLinn
This is probably what's happening: https://wiki.haskell.org/GHC/TypeSigsAndAmbiguity On 05/05/2017 05:55 AM, MarLinn wrote:
Hi,
I've been working on a kind of constrained version of Data.Dynamic:
data Dynamic (c :: * -> Constraint) where Dynamic :: (Typeable a, c a) => a -> Dynamic c
The idea is that Data.Dynamic gives up all compile time type information. In this variant I can at least keep a bit of the information around that I have. (In fact I can even "lift" a type into a constraint, thereby keeping /all/ information.) Most of my functions are nailed down, including mappings and traversals. But one group of functions eludes me: functions to change only the constraint, while keeping the value. Here is one of my goal types:
castDynamic :: ( Typeable a, c a, d a ) => Dynamic c -> Dynamic d
I'm pretty sure I'll have to sprinkle in a Proxy a, but so be it. I've thrown all typing tricks at this function that I know of, from unsafeCoerce over case-of instead of pattern matching, to ScopedTypeVariables. But I couldn't convince ghci to accept my code. So I tried something simpler.
castDynamic' :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)
Here's where it gets funny: I can implement this function in ghci interactively just fine.
:t \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)
But when I enter the exact same code in a file and load it, ghci balks at me because a is too ambiguous. Again, I've tried if it's the monomorphism restriction, or if I need to sprinkle in more (scoped) signatures or explicit forall's etc… nothing helped.
What is the difference here? Am I missing an extension? Am I doing something I shouldn't and the interactive mode is just doing me a favor? There was a discussion on this list less than a month ago where it was mentioned that ghci handles polymorphic types differently depending on the source of the code. Is there some documentation on these differences? Any help would be appreciated.
Cheers, MarLinn
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (3)
-
David Kraeutmann -
MarLinn -
Matt