Re: [Haskell-cafe] [Haskell] Higher types in contexts

moved to haskell-cafe On Mon, 5 Mar 2012, Barney Hilken wrote:
Is there any deep reason why I can't write a polymorphic type in a context? I think the record update problem can be (sort of) solved if you could write:
class Has r Rev (forall a. [a] -> [a]) => HRClass r where setHRClass :: (forall a.[a] -> [a]) -> r -> r
but polymorphic types are not allowed in contexts. Is this one of the problems SPJ considers "Hard" or is it a feasible extension?
I don't know what you want to do, but you may wrap the (forall a. [a] -> [a]) in an existential type: data ListFunc = forall a. ListFunc ([a] -> [a]) class Has r Rev ListFunc => HRClass r where setHRClass :: ListFunc -> r -> r

I don't know what you want to do, but you may wrap the (forall a. [a] -> [a]) in an existential type:
data ListFunc = forall a. ListFunc ([a] -> [a])
class Has r Rev ListFunc => HRClass r where setHRClass :: ListFunc -> r -> r
Thanks Henning, What we're wanting to do is set the Higher-ranked function into a record type, then get it and apply it polymorphically. SPJ's example is: data HR = HR { rev :: forall a. [a] -> [a] } -- where rev is the label for the H-R function f :: HR -> ([Bool], [Char]) f r = (r.rev [True], r.rev "hello") -- where r.rev is new syntax to get the func from HR I've tried that ListFunc wrapping you suggest: data HR = HR { rev :: ListFunc } rHR1 = HR{ rev = ListFunc reverse } -- put the `reverse` function into the record type -- the setHRClass method would do this But I can't 'dig out' the H-R function and apply it (not even monomorphically): case (rev rHR1) of { (ListFunc fn) -> fn "hello" } ==> Couldn't match type `a' with `Char' `a' is a rigid type variable bound by a pattern with constructor ListFunc :: forall a. ([a] -> [a]) -> ListFunc, in a case alternative at <interactive>:0:25 Expected type: [a] Actual type: [Char] SPJ's approach (without a wrapper, but with some fancy instance constraints) can 'dig out' the function and apply it polymorphically, but he can't get the function into the record without using an explicit data constructor. What am I doing wrong? AntC -- View this message in context: http://haskell.1045720.n5.nabble.com/Re-Haskell-Higher-types-in-contexts-tp5... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

On 3/5/12 5:13 PM, AntC wrote:
I've tried that ListFunc wrapping you suggest: [...] But I can't 'dig out' the H-R function and apply it (not even monomorphically):
That's because the suggestion changed it from a universal quantifier to an existential quantifier. data Exists f = forall a. Exists (f a) data Forall f = Forall (forall a. f a) With Exists, we're essentially storing a pair of the actual type 'a' and then the f a itself. We can't just pull out the f a and use it, because we don't know what 'a' is. We can bring it into scope temporarily by case matching on the Exists f, which allows us to use polymorphic functions, but we still don't actually know what it is so we can *only* use polymorphic functions. Conversely, with Forall we're storing some f a value which is in fact polymorphic in 'a'. Here, because it's polymorphic, the caller is free to choose what value of 'a' they would like the f a to use. Indeed, they can choose multiple different values of 'a' and get an f a for each of them. -- Live well, ~wren

I find it easy to understand this distinction by writing out the types of
the constructors and case expressions for these objects, in a language like
system F:
(here, {x :: t} means a type argument with name x of kind t)
Exists :: {f :: *->*} -> {a :: *} -> f a -> Exists f
Forall :: {f :: *->*} -> ({a :: *} -> f a) -> Forall f
Notice the higher rank type in the constructor 'Forall'.
Similarly, the case deconstruction for these:
caseExists :: {r :: *} -> {f :: *->*} -> ({a :: *} -> f a -> r) -> Exists f
-> r
caseForall :: {r :: *} -> {f :: *->*} -> (({a :: *} -> f a) -> r) -> Forall
f -> r
The function passed to caseExists needs to be able to handle any type 'a'
we throw at it, whereas the function passed to caseForall can choose what
'a' it wants to use (and can choose multiple different 'a's by calling the
({a::*} -> f a) parameter function multiple times. In the simple case that
the case function only instantiates 'a' at a single type, we can simplify
this:
caseForall' :: {r :: *} -> {f :: * -> *} -> {a :: *} -> (f a -> r) ->
Forall f -> r
and this function is definable in terms of caseForall:
caseForall' {r} {f} {a} k v = caseForall {r} {f} (\mk_fa -> k (mk_fa {a})) v
-- ryan
On Mon, Mar 5, 2012 at 9:37 PM, wren ng thornton
On 3/5/12 5:13 PM, AntC wrote:
I've tried that ListFunc wrapping you suggest: [...]
But I can't 'dig out' the H-R function and apply it (not even monomorphically):
That's because the suggestion changed it from a universal quantifier to an existential quantifier.
data Exists f = forall a. Exists (f a)
data Forall f = Forall (forall a. f a)
With Exists, we're essentially storing a pair of the actual type 'a' and then the f a itself. We can't just pull out the f a and use it, because we don't know what 'a' is. We can bring it into scope temporarily by case matching on the Exists f, which allows us to use polymorphic functions, but we still don't actually know what it is so we can *only* use polymorphic functions.
Conversely, with Forall we're storing some f a value which is in fact polymorphic in 'a'. Here, because it's polymorphic, the caller is free to choose what value of 'a' they would like the f a to use. Indeed, they can choose multiple different values of 'a' and get an f a for each of them.
-- Live well, ~wren
______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe
participants (4)
-
AntC
-
Henning Thielemann
-
Ryan Ingram
-
wren ng thornton