Hunting for ghci manual input vs. file input differences again

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Hunting for ghci manual input vs. file input differences again

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.
Reply | Threaded
Open this post in threaded view
|

Re: Hunting for ghci manual input vs. file input differences again

Matt
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.


Matt Parsons

On Thu, May 4, 2017 at 9:55 PM, MarLinn <[hidden email]> 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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Hunting for ghci manual input vs. file input differences again

David Kraeutmann
In reply to this post by 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Hunting for ghci manual input vs. file input differences again

MarLinn
In reply to this post by Matt

> 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
_______________________________________________
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.