Re: [Haskell-cafe] help with type variable escaping scope/passing lens as function argument

Thanks so much! You just taught me many things I didn't know! The code is working by the way. :) On Dec 31, 2016 3:59 AM, "Li-yao Xia" wrote:

Hi Cody,

I forgot to keep Haskell-cafe in copy.

...

Are you saying that my forall applies to both a and b, but not only a? And that a is what (Lens (Record rs) Chicago -> (...)) expands to?

That sounds about right.

Try this:

dateBetween :: (forall f. Functor f => (Chicago -> f Chicago) -> Record rs -> f (Record rs)) -> Day -> Day -> Pipe (Record rs) (Record rs) IO m

Or, a bit refactored:

type Lens s a = forall f. Functor f => (a -> f a) -> (s -> f s)

dateBetween :: Lens (Record rs) Chicago -> Day -> Day -> Pipe (Record rs) (Record rs) IO m

...

Where does f1 come from? Does GHC just come up with it because my type variable doesn't satisfy it?

When you write this

dateBetween :: forall (rs :: [*]) (m :: *) (f :: * -> *). (Functor f) => ((Chicago -> f Chicago) -> Record rs -> f (Record rs)) -> Day -> Day -> Pipe (Record rs) (Record rs) IO m dateBetween target start end = ...

The parameter target is a monomorphic function, with f instantiated at the call site of dateBetween. This means that dateBetween can not assume anything about f apart from the fact that it is an instance of Functor, i.e., f must be abstract.

Then we have:

let targetDate = rget target r

but this is the type of rget:

rget :: (forall f . Functor f => (a -> f a) -> Record rs -> f (Record rs)) -> Record rs -> a

rget expects a polymorphic function, while target is monomorphic. The compiler tries to unify "f" from the type signature of dateBetween, and "f" from the type signature of rget. To avoid confusion, the compiler does renaming, so that different variables (identified by where they are bound) have different names, and that's where "f1" comes from:

rget :: forall a1 rs1. (forall f1 . Functor f1 => (a1 -> f1 a1) -> Record rs1 -> f1 (Record rs1)) -> Record rs1 -> a1

Applying rget to (target :: (Chicago -> f Chicago) -> Record rs -> f (Record rs)), the compiler tries to unify f and f1, and fails because they are "rigid", meaning, they can't be instantiated. f is rigid because it is abstract in the body of dateBetween, f1 is rigid because it is the type parameter of the polymorphic function rget expects.

Li-yao

On 12/31/2016 09:07 AM, Cody Goodman wrote:

...

Hi Li-yao,

Are you saying that my forall applies to both a and b, but not only a? And that a is what (Lens (Record rs) Chicago -> (...)) expands to?

In either case, I don't understand what action I can take based on what was you said and what I understand from it :/

Where does f1 come from? Does GHC just come up with it because my type variable doesn't satisfy it?

Thanks,

Cody

On Sat, Dec 31, 2016 at 2:54 AM, Li-yao Xia wrote:

Hi Cody,

...

You wrote something of the shape

forall f. Functor f => a -> b

which means

forall f. Functor f => (a -> b)

but not

(forall f. Functor f => a) -> b

which would be what (Lens (Record rs) Chicago -> (...)) expands to.

Regards, Li-yao

On 12/31/2016 08:45 AM, Cody Goodman wrote:

Thanks for the help Li-yao, but I still have a type error after using

...

Rank N Types. I have updated my code on github https://github.com/codygman/frames-credit-card-trans-demo/bl ob/master/src/Main.hs#L45() and pasted below:

dateBetween :: forall (rs :: [*]) (m :: *) (f :: * -> *). (Functor f) => ((Chicago -> f Chicago) -> Record rs -> f (Record rs)) -> Day -> Day -> Pipe (Record rs) (Record rs) IO m dateBetween target start end = P.filter go where go :: Record rs -> _ go r = let targetDate = (rget target r) :: Chicago targetDate' = chicagoToZoned targetDate :: ZonedTime targetDay = localDay (zonedTimeToLocalTime targetDate') :: Day in targetDay >= start && targetDay < end -- type error -- src/Main.hs:53:39: error: … -- • Couldn't match type ‘f’ with ‘f1’ -- ‘f’ is a rigid type variable bound by -- the type signature for: -- dateBetween :: forall (rs :: [*]) m (f :: * -> *). -- Functor f => -- ((Chicago -> f Chicago) -> Record rs -> f (Record rs)) -- -> Day -> Day -> Pipe (Record rs) (Record rs) IO m -- at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:45:45 -- ‘f1’ is a rigid type variable bound by -- a type expected by the context: -- forall (f1 :: * -> *). -- Functor f1 => -- (Chicago -> f1 Chicago) -> Record rs -> f1 (Record rs) -- at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:53:34 -- Expected type: (Chicago -> f1 Chicago) -- -> Record rs -> f1 (Record rs) -- Actual type: (Chicago -> f Chicago) -> Record rs -> f (Record rs) -- • In the first argument of ‘rget’, namely ‘target’ -- In the expression: (rget target r) :: Chicago -- In an equation for ‘targetDate’: -- targetDate = (rget target r) :: Chicago -- • Relevant bindings include -- target :: (Chicago -> f Chicago) -> Record rs -> f (Record rs) -- (bound at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:51:13) -- dateBetween :: ((Chicago -> f Chicago) -- -> Record rs -> f (Record rs)) -- -> Day -> Day -> Pipe (Record rs) (Record rs) IO m -- (bound at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:51:1) -- Compilation failed.

On Sat, Dec 31, 2016 at 2:21 AM, Li-yao Xia wrote:

Hello Cody,

...

Complete the type annotation, using RankNTypes

dateBetween :: Lens Record Chicago -> ...

GHC does not infer higher-rank types, because it is an undecidable problem in general, so you must annotate polymorphic parameters explicitly.

Regards, Li-yao

On 12/31/2016 07:56 AM, Cody Goodman wrote:

I have the following code and error(also seen at

...

https://github.com/codygman/frames-credit-card-trans-demo/bl ob/master/src/Main.hs#L28 ):

-- between meaning on or after start but before end dateBetween :: _ -> Day -> Day -> Pipe (Record rs) (Record rs) IO r dateBetween target start end = P.filter go where go :: Record rs -> _ go r = let targetDate = rget target r :: Chicago targetDate' = chicagoToZoned targetDate :: ZonedTime targetDay = localDay (zonedTimeToLocalTime targetDate') :: Day in targetDay >= start && targetDay < end -- type error -- src/Main.hs:48:38: error: … -- • Couldn't match expected type ‘(Chicago -> f Chicago) -- -> Record rs1 -> f (Record rs1)’ -- with actual type ‘t’ -- because type variable ‘f’ would escape its scope -- This (rigid, skolem) type variable is bound by -- a type expected by the context: -- Functor f => (Chicago -> f Chicago) -> Record rs1 -> f (Record rs1) -- at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:48:33-45 -- • In the first argument of ‘rget’, namely ‘target’ -- In the expression: rget target r :: Chicago -- In an equation for ‘targetDate’: -- targetDate = rget target r :: Chicago -- • Relevant bindings include -- r :: Record rs1 -- (bound at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:48:12) -- go :: Record rs1 -> Bool -- (bound at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:48:9) -- target :: t -- (bound at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:46:13) -- dateBetween :: t -> Day -> Day -> Pipe (Record rs) (Record rs) IO r -- (bound at /home/cody/source/frames-credit-card-trans-demo/src/Main.hs:46:1) -- Compilation failed.

Perhaps it's late, but I'm fairly sure I've done something like this before.

Thanks,

Cody

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