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

Cody Goodman codygman.consulting at gmail.com
Sat Dec 31 17:04:08 UTC 2016


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" <li-yao.xia at ens.fr> 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 <li-yao.xia at ens.fr> 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 <li-yao.xia at ens.fr> 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.
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161231/0fb74dae/attachment.html>


More information about the Haskell-Cafe mailing list