[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