How to use a proxy in Haskell? (probably using a h

2019-06-22 09:57发布

问题:

For the last few months, I've been putting some serious effort into learning Haskell - previously, I was a seemingly perpetual newbie with a very limited knowledge of the basics. While trying to put my new knowledge into practice on few-steps-up-from-hello-world projects, I keep finding that I want to use proxy-like patterns based on type classes. The first couple of times, when I figured out why it wasn't working, I dismissed it as "OK - I may not find a single idiomatic Haskell replacement, but odds are the problem here is that I'm using the wrong approach for the language". But what I've found is that I really really don't like not being able to do proxy-like things.

Trying to get a deeper understanding of why I couldn't use a proxy, after lots of experimenting, I finally figured out that with GHCs higher rank types extension, perhaps I can have proxies. But I still can't quite make it work, and I'm not sure why.

Here is the code for the best I've managed...

{-# LANGUAGE RankNTypes #-}
module Test where

--  Simple type class based on parser combinators.
class Gen g where
  get :: g x -> [(x, g x)]

instance Gen [] where
  get [] = []
  get (x:xs) = [(x, xs)]

--  Proxy type - holds a pair containing...
--    - a value of some type that supports Gen
--    - a function to indicate when an item should be skipped
newtype PROXY nestedgen x = Proxy (nestedgen x, x -> Bool)

proxyskip :: Gen nestedgen => PROXY nestedgen r -> Bool
proxyskip (Proxy (g, predf)) = case get g of
                                 []        -> False
                                 ((r,_):_) -> predf r

proxyget :: Gen nestedgen => PROXY nestedgen r -> [(r, PROXY nestedgen r)]
proxyget pr@(Proxy (sg, predf)) = if proxyskip pr
                                    then [(r2, g2) | (_, g1) <- get sg, (r2,g2) <- proxyget (Proxy (g1, predf))]
                                    else [(r3, Proxy (g3, predf)) | (r3,g3) <- get sg]

--  Instance of Gen for PROXY - get skips items where appropriate
instance Gen nestedgen => Gen (PROXY nestedgen) where
  get = proxyget

--  Test "parser"
--  Get the specified number of items, providing them as a list (within
--  the list of nondeterministic (result, state) pairs).
getN :: Gen g => Int -> g x -> [([x], g x)]
getN n g | (n < 0)  = error "negative n"
         | (n == 0) = [([], g)]
         | True     = [(r1:r2, g2) | (r1, g1) <- get g, (r2, g2) <- getN (n-1) g1]

--  Wrap some arbitrary "parser" in a PROXY that skips over the letter 'l'
proxyNotL :: Gen gb => gb Char -> PROXY gb Char
proxyNotL gg = (Proxy (gg, \ch -> (ch /= 'l')))

call_f0 :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)]
call_f0 f0 g0 = f0 (proxyNotL g0)

test :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, gb Char)]
test f0 g0 = [(r, g2) | (r, Proxy (g2, _)) <- call_f0 f0 g0]

The last remaining error occurs on the line call_f0 f0 g0 = f0 (proxyNotL g0)...

[1 of 1] Compiling Test             ( Test.hs, Test.o )

Test.hs:44:21:
    Could not deduce (ga ~ PROXY gb)
    from the context (Gen gb)
      bound by the type signature for
                 call_f0 :: Gen gb =>
                            (Gen ga => ga Char -> [(r, ga Char)])
                            -> gb Char
                            -> [(r, PROXY gb Char)]
      at Test.hs:44:1-33
      `ga' is a rigid type variable bound by
           the type signature for
             call_f0 :: Gen gb =>
                        (Gen ga => ga Char -> [(r, ga Char)])
                        -> gb Char
                        -> [(r, PROXY gb Char)]
           at Test.hs:44:1
    Expected type: ga Char
      Actual type: PROXY gb Char
    In the return type of a call of `proxyNotL'
    In the first argument of `f0', namely `(proxyNotL g0)'
    In the expression: f0 (proxyNotL g0)

Looking at the problematic function...

call_f0 :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)]
call_f0 f0 g0 = f0 (proxyNotL g0)

The f0 function is (if I understand higher rank types correctly) a polymorphic function passed as a parameter, with type Gen ga => ga Char -> [(r, ga Char)]. In translating-to-C terms, the caller has passed in a function pointer, but has not supplied the vtable pointer.

The proxyNotL function returns something of type PROXY gb Char, and there's an instance declaration instance Gen nestedgen => Gen (PROXY nestedgen) where ..., so that PROXY gb Char instances Gen provided gb instances Gen, which it does according to the type signature for call_f0.

Basically, as far as I can tell, GHC should say "can I provide the vtable that f0 requires... hmmm... yes, since PROXY gb instances Gen, and I know about PROXY and gb, yes I can".

So... why is GHC refusing to unify ga and Proxy gb? Why is GHC refusing to call a polymorphic function, with an argument value that should be supported by the polymorphic type of that function?

Or alternatively, what am I completely misunderstanding here?

回答1:

You just need to explicitly specify that the function f0 must be polymorphic by adding the universal quantifier forall ga. to your type signatures:

call_f0 :: Gen gb => (forall ga. Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)]
test :: Gen gb => (forall ga. Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, gb Char)]

Otherwise, GHC will put an implicit forall ga. at the outermost level, meaning that the caller would get to decide which ga should be used, while GHC has correctly deduced that these functions must be able to choose themselves that ga should be PROXY gb.

In other words, when using RankNTypes to require a polymorphic argument, you must always use an explicit quantifier to specify this.



回答2:

I am not quite sure what you mean by "proxy" in this context. But I gather you may mean a data type representing instances of Gen.

Taking the Gen typeclass

class Gen g where
    get :: g x -> [(x, g x)]

the type forall g. Gen g => g x should be representable by a concrete data type (constructor). If you have such a value, say a, the only valid operation is to apply get, giving us:

a :: forall g. Gen g => g x
get a :: forall g. [(x, g x)]

So we see that the information contained in g x is the same as the information contained in [(x, g x)]; if we want a type that can represent any such g, we take the greatest fixed point:

newtype G x = G { unG :: [(x, G x)] }

G should now be able to represent any Gen

toG :: Gen g => g x -> G x
toG = G . map (second toG) . get

and it is itself an instance of Gen

instance Gen G where
    get (G as) = as

Is that anything like what you wanted?