[Haskell-cafe] help with type variable escaping scope/passing lens as function argument
Li-yao Xia
li-yao.xia at ens.fr
Sat Dec 31 09:59:46 UTC 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 <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.
>>>>>
>>>>>
>>>>>
>>>
>
More information about the Haskell-Cafe
mailing list