Error on dictionary passing on either where and let declaration

[YoEight]

Firstly the issue's title might be misleading, it's just a supposition.

Lately, I was porting Pipe library to Frege. I'm not a fan of how Pipes are currently encoded in Haskell, I use CPS instead.

Here's some code

data Proxy a' a b' b m r = Proxy { runProxy :: forall c.
                                   (r  -> m c) ->                                -- Yield r
                                   (a' -> (a  -> Proxy a' a b' b m r) -> m c) -> -- Request a' (a  -> Proxy a' a b' b m r))
                                   (b  -> (b' -> Proxy a' a b' b m r) -> m c) -> -- Respond b  (b' -> Proxy a' a b' b m r))
                                    m c
                                 }

instance Functor (Proxy a' a b' b m) where
  fmap f (Proxy k) = Proxy go
    where                                                                                                                                                               
      go ky kq kp = 
        let onRequest a' q = kq a' (fmap f . q)                                                                                                                                                                      
            onRespond b  p = kp b  (fmap f . p)                                                                                                                                                           
        in k (ky . f) onRequest onRespond

Sadly, it doesn't compile unlike in Haskell. Here's the compiler output

E proxy.fr:18: function `onRespond{2819}` has context Functor (Proxy γ β δ α
    ζ) =>
E proxy.fr:17: function `onRequest{2818}` has context Functor (Proxy γ β δ α
    ζ) =>

I'm using frege3.20.42.jar

Any idea ?

[Ingo60]

Indeed, it doesn't make a difference whether it is let or where as where is just a syntactically different way to write a let. There is a chart in the Haskell 2010 Report that shows how case expressions with pattern guards and where clauses are transformed to simple case expressions without pattern guards and where clauses, the same chart is also in the Frege Language document. Add to this that a single line definition like

foo = bar where baz

is treated like

foo = case () of () | true -> bar where baz

Now to the problem at hand: I know that I had assumed that on local functions there can be no class constraints on their own, rather, class constraints should be "handed up" and appear eventually in the type signature of the top level function only. This helps - at runtime - to avoid (constrcuting and) passing one and the same dictionary around, which should be already in scope anyhow as argument of the outer function.

It now looks like either a) this assumption was wrong or b) there is an error in the typechecker.

I will look into it a bit deeper tonight, and hope it is the latter (after all, there is already a Functor (Proxy ...) dictionary in place, isn't it, why is that one not being used?). Meanwhile, it could help if you decorate all definitions with type signatures as far as possible, to help me understand what is going on here. If it is not possible to give a valid type signature, write it at least as comment.

[YoEight]

I've tried to reduce the problem at the utmost but failed. I'll work on this tonight too and I''ll annotate type signature in a hour.

[Ingo60]

Things you could try:

• write onrequest and onresponse as lambda expressions
• Add f and k as arguments to go and give go as separate function outside of the instance definition, if only to see if the inferred type is correct (on the command line, give option -explain n where n is the line number where go is defined).

[YoEight]

Hope it could help written like this:

data Proxy a' a b' b m r = Proxy { runProxy :: forall c.
                                   (r  -> m c) ->                                -- Yield r
                                   (a' -> (a  -> Proxy a' a b' b m r) -> m c) -> -- Request a' (a  -> Proxy a' a b' b m r))
                                   (b  -> (b' -> Proxy a' a b' b m r) -> m c) -> -- Respond b  (b' -> Proxy a' a b' b m r))
                                    m c
                                 }

instance Functor (Proxy a' a b' b m) where
  -- f :: r -> s
  fmap f (Proxy k) = Proxy go
    where
      go :: forall c.
             (s -> m c)
              -> (a' -> (a  -> Proxy a' a b' b m s) -> m c) 
              -> (b  -> (b' -> Proxy a' a b' b m s) -> m c)
              -> m c                                                                                                                                                  
      go ky kq kp = 
        let onRequest :: a' -> (a  -> Proxy a' a b' b m r) -> m c
            onRequest a' q = kq a' (fmap f . q)   -- (fmap f) :: Proxy a' a b' b m r -> Proxy a' a b' b m s      
                                                  -- q :: a  -> Proxy a' a b' b m r
                                                  -- kq :: a' -> (a -> Proxy a' a b' b m s)
            onRespond :: b -> (b' -> Proxy a' a b' b m r) -> m c                                                                                                                                                            
            onRespond b  p = kp b  (fmap f . p)  -- (fmap f) :: Proxy a' a b' b m r -> Proxy a' a b' b m s
                                                 -- p:: b'  -> Proxy a' a b' b m r
                                                 -- kp :: b -> (b' -> Proxy a' a b' b m s)
        -- ky :: s -> m c 
        -- ky . f :: r -> m c                                                                                                                                                         
        in k (ky . f) onRequest onRespond

[Ingo60]

The first thing I noticed is that our functions that are supposed to show types nicely are broken and do not work wery well for function types nested in function types.

Second, the types of onRequest and onRespond cannot be written down, because they contain the type called here c as monomorphic type variable, that somehow appears in go.

Anyway, the code appears to be well typed, question is only why does it not take over the Functor constraint appearing in onRequest/onRespond.

I try to provoke the same situation in an easier program where I have better overview.

[YoEight]

Like you've suggested, I've rewrote the code using lambdas. This works like a charm.

data Proxy a' a b' b m r = Proxy { runProxy :: forall c.
                                   (r  -> m c) ->
                                   (a' -> (a  -> Proxy a' a b' b m r) -> m c) ->
                                   (b  -> (b' -> Proxy a' a b' b m r) -> m c) ->
                                   m c
                                 }

instance Functor (Proxy a' a b' b m) where
  fmap f (Proxy k) = Proxy go
    where
      go ky kq kp = k (ky . f) (\a' \q -> kq a' (fmap f . q)) (\b \p -> kp b (fmap f . p))

Ironically, that was how I wrote it the first time

[Ingo60]

Damn! Referential transparency, there you go!

[YoEight]

Note the code gets really funky when defining Applicative and Monad instances with only lambdas :)

[YoEight]

I've tried to pass f and k as arguments to a separate function

instance Functor (Proxy a' a b' b m) where
  fmap f (Proxy k) = mapProxy f k

mapProxy :: forall c.
            (r -> s)
            -> ((r  -> m c) -> (a' -> (a  -> Proxy a' a b' b m r) -> m c) -> (b  -> (b' -> Proxy a' a b' b m r) -> m c) -> m c)
            -> Proxy a' a b' b m s
mapProxy f k = Proxy (\ky \kq \kp -> k (ky . f) (\a' \q -> kq a' (fmap f . q)) (\b \p -> kp b (fmap f . p)))

But I had this error

bash-3.2$ java -Xss1m -jar fregec.jar -explain 14 -d build proxy-test.fr
E proxy-test.fr:14: free type variable(s) b', a', a, b, r, m, s not allowed

[Ingo60]

It happens because both in onRequest and onResponse it uses a type variable in place of (Proxy ....) and infers constraint (Functor t2888 => ...). So to speak, in typechecking onRequest, the type checker doesn't know yet that t2888 will only later be unified with (Proxy .....). Would it know this earlier, it could easily discharge the constraint because it is already known that Proxy .... is a Functor. This means, the constraint is indeed handed upwards, but is apparently later discharged in "go" as soon as the type variable gets unified with (Proxy .....). This is my diagnosis up to now, I'll have to invest still more time to fully understand the case. However, I managed to construct the following smaller example:

data T x = T { x :: x, y :: forall y . x -> T y }

instance Show (T x) where
    show (T x f) = fst ("T", go (f x)) 
         where
              go t  = fst (show t, x)

The trick seems to be to first cause an innocent looking type like

go :: Show t2345 => t2345 -> String

and to substitute t2345 with some type that happens to satisfy the constraint later. This, however, does only work when the let bound function mentions some variable from outer scopes and thus cannot be quantified. This is why I need to mention x in go, otherwise the error does not show up.

This gives us also a hint for a better workaround than the lambda thing: just pass f and kq or kp explicitly to onRequest and onRespond so that there are no free variables anymore inside them. (Contrary to intuition, this will even give faster code, as there will be no need to build anonymous inner classes, as both functions now are silently moved to the top level and result in a static java method. (At least I think that passing 3 additional arguments (dictionary + f + kq or kp) is faster than creating a closure that closes over those 3 values. But I may err here.))

Nevertheless, I'll try to fix that later, because the referential transparency must not get lost.

[Ingo60]

Your attempt is indeed wrong. On the outer level, either mention all type variables in forall, or drop the forall altogether (which is a shorthand for the former).

[Ingo60]

It works even shorter and without higher rank polymorphism (thank God!):

data T x = T { x :: x }

instance Show (T x) where
    show (T x) = fst ("T", go (T x)) 
        where
            go t  = x `seq` show t

[YoEight]

You're right, it's working now. About the problem, I'll use lambdas until a fix comes.