New subject: help with type variable escaping scope/passing lens as function argument

31 Dec 2016

      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.

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

Li-yao Xia

Cody Goodman

tags

participants (2)