an instance in other than the last type parameters
Hi, I have probably a very simple question, but I wasn't able to figure it out myself. Consider a two-parameter data type:
data X a b = X a b
If I want to make it a functor in the last type variable (b), I can just define
instance Functor (X a) where fmap f (X a b) = X a (f b)
But how do I write it if I want X to be a functor in its first type variable? Is that possible at all? Something like:
instance Functor ??? where fmap f (X a b) = X (f a) b
Thanks in advance, Petr
Petr,
If I want to make it a functor in the last type variable (b), I can just define
instance Functor (X a) where fmap f (X a b) = X a (f b)
But how do I write it if I want X to be a functor in its first type variable?
Short answer: you can't. Easiest way to workaround is to define a newtype wrapper around your original datatype: newtype X' b a = X' {unX' :: X a b} instance Functor (X' b) where fmap g (X' (X a b)) = X' (X b (g a)) Cheers, Stefan
Petr,
Short answer: you can't. Easiest way to workaround is to define a newtype wrapper around your original datatype:
newtype X' b a = X' {unX' :: X a b}
instance Functor (X' b) where fmap g (X' (X a b)) = X' (X b (g a))
Err.... fmap g (X' (X a b)) = X' (X (g a) b) Cheers, Stefan
Can anyone explain the theoretical reason for this limitation, ie other than
it is a syntactical restriction, what would it take to lift this restriction
?
----- Original Message -----
From: "Stefan Holdermans"
Petr,
If I want to make it a functor in the last type variable (b), I can just define
instance Functor (X a) where fmap f (X a b) = X a (f b)
But how do I write it if I want X to be a functor in its first type variable?
Short answer: you can't. Easiest way to workaround is to define a newtype wrapper around your original datatype:
newtype X' b a = X' {unX' :: X a b}
instance Functor (X' b) where fmap g (X' (X a b)) = X' (X b (g a))
Cheers,
Stefan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Ack, missed the reply-all button...] This was part of my motivation behind the 'removing polymorphism from Functor' thing... to select a different parameter we'd essentially need type-level lambdas... I'll use 'Λ' (capital lambda) for it: instance Functor (Λ a. X a b) where fmap f (X a b) = X (f a) b We don't have these [1], but we *do* have type families, which are kind of like type-level lambdas turned 'inside out' (at least to my eyes), so my idea was to separate this out: type family Point :: * type instance Point (X a b) = a class Functor f where fmap :: (Point f -> Point f) -> f -> f Here I began to run into problems which are a bit irrelevant to this discussion :) [1]: I'm not sure of the exact connection, but see, e.g. Oleg's construction of computation at the type level (http://okmij.org/ftp/Haskell/TypeLC.lhs), wherein he notes the "primary role of type application rather than that of abstraction". - George
John Lask wrote:
Can anyone explain the theoretical reason for this limitation, ie other than it is a syntactical restriction, what would it take to lift this restriction ?
There are a couple of theoretical concerns, mainly that full type-level lambdas can lead down a rocky path (though simple combinators like `flip` and `const` are fine, and that's all we'd need for most cases). But by and large it's just a syntactic restriction. -- Live well, ~wren
On Thu, Jul 23, 2009 at 9:01 PM, wren ng thornton
John Lask wrote:
Can anyone explain the theoretical reason for this limitation, ie other than it is a syntactical restriction, what would it take to lift this restriction ?
There are a couple of theoretical concerns, mainly that full type-level lambdas can lead down a rocky path (though simple combinators like `flip` and `const` are fine, and that's all we'd need for most cases). But by and large it's just a syntactic restriction.
I wouldn't say it's "just" a syntactic restriction. I'm pretty sure
unrestricted type lambdas are incompatible with Haskell's class
system. Otherwise, you might end up with Functor instances for /\b.
(a,b) and /\a. (a,b), at which point fmap (+1) (1,2) is ambiguous.
--
Dave Menendez
David Menendez wrote:
wren ng thornton wrote:
John Lask wrote:
Can anyone explain the theoretical reason for this limitation, ie other than it is a syntactical restriction, what would it take to lift this restriction ?
There are a couple of theoretical concerns, mainly that full type-level lambdas can lead down a rocky path (though simple combinators like `flip` and `const` are fine, and that's all we'd need for most cases). But by and large it's just a syntactic restriction.
I wouldn't say it's "just" a syntactic restriction. I'm pretty sure unrestricted type lambdas are incompatible with Haskell's class system. Otherwise, you might end up with Functor instances for /\b. (a,b) and /\a. (a,b), at which point fmap (+1) (1,2) is ambiguous.
This is essentially the same problem as arises with overlapping instances. It is a new version of that problem since it introduces new places for overlapping (by highlighting the fact that instances on a *->* kind are actually instances on type-level lambdas), but the problem isn't exactly a new one. A tweak of the overlap detector should be able to catch these too; eta expand and check for overlap of the type-level terms. The definition of "overlap" is somewhat different since it must respect abstraction, but it's not too much different than the current version. It is still possible to use type signatures to clear things up, albeit much uglier than usual. If we were to head down the road of type-level lambdas then we would want some mechanism for making it easier to deal with bifunctors like (,) and similar issues. The easiest thing, perhaps, would be to expose some of the explicit type passing that happens in the System F core[1], though we'd want to massage the dictionary-passing so that we could say things like (fmap @A) to mean the fmap of the instance for A. So yes, implementing type-level lambdas is more than just changing the parser (so more than "just" syntax), but provided the right restrictions on what type-level lambdas are acceptable I don't think there are any substantial theoretical issues (so I'd say it's just syntax, rather than theoretical concerns). And these restrictions are the obvious ones, mainly blocking recursion to prevent the compiler from hanging or generating infinite types. [1] In System F the capital-lambda binder is used for the term-level abstraction of passing type representations. So for example we have, id :: forall a. a -> a id = /\a. \(x::a). x Thus, the forall keyword is serving as the type-level abstraction. Perhaps this is suboptimal syntax, but it is the standard. We could, of course, have both a term-level /\ and a type-level /\ where the latter is the type of the former (since the namespaces are separate) though that's also dubious. Capital-pi is the canonical type-level abstraction, though that evokes the idea of dependent types which are much more complex. -- Live well, ~wren
wren ng thornton wrote:
[1] In System F the capital-lambda binder is used for the term-level abstraction of passing type representations. So for example we have,
id :: forall a. a -> a id = /\a. \(x::a). x
Thus, the forall keyword is serving as the type-level abstraction. Perhaps this is suboptimal syntax, but it is the standard. We could, of course, have both a term-level /\ and a type-level /\ where the latter is the type of the former (since the namespaces are separate) though that's also dubious. Capital-pi is the canonical type-level abstraction, though that evokes the idea of dependent types which are much more complex.
What do you mean by "type-level abstraction" here? In a language with type functions and polymorphism, we need three different lambda binders: (1) abstraction over terms in terms (to construct functions) (2) abstraction over types in terms (to construct polymorphic values) (3) abstraction over types in types (to construct type functions) I think only (2) should be written as upper-case lambdas, while (1) and (3) should both be written as lower-case lambdas. Since (1) and (3) belong to different syntactic categories, they can not be confused, and we can reuse the lower-case lambda at the type-level. Furthermore, we need three function types / kinds to describe the three lambdas one level higher: (4) the type of functions (5) the type of polymorphic values (6) the kind of type functions In ghc, we already have "forall" for (5), and arrows for (4) and (6). I would say that (3) is the "type-level abstraction", not (5). Tillmann
Tillmann Rendel wrote:
wren ng thornton wrote:
[1] In System F the capital-lambda binder is used for the term-level abstraction of passing type representations. So for example we have,
id :: forall a. a -> a id = /\a. \(x::a). x
Thus, the forall keyword is serving as the type-level abstraction. Perhaps this is suboptimal syntax, but it is the standard. We could, of course, have both a term-level /\ and a type-level /\ where the latter is the type of the former (since the namespaces are separate) though that's also dubious. Capital-pi is the canonical type-level abstraction, though that evokes the idea of dependent types which are much more complex.
What do you mean by "type-level abstraction" here?
I mean an abstraction, as in a lambda-abstraction (aka a lambda-expression), at the type level.
In a language with type functions and polymorphism, we need three different lambda binders:
(1) abstraction over terms in terms (to construct functions) (2) abstraction over types in terms (to construct polymorphic values) (3) abstraction over types in types (to construct type functions)
I think only (2) should be written as upper-case lambdas, while (1) and (3) should both be written as lower-case lambdas. Since (1) and (3) belong to different syntactic categories, they can not be confused, and we can reuse the lower-case lambda at the type-level.
I'm sure that's fine. I was merely pointing out precedent. The syntax of #3 could also be conflated with the syntax of #2, for the same reason: they are in different syntactic categories. I pointed this out because the capital-lambda was the syntax others in the thread were using. Also, it makes sense to me to have #2 and #3 ("abstraction over types in _") paired together, rather than #1 and #3 ("abstraction over X in X"). Pairing #2/#3 also gives term/type symmetry as we have for other built-ins like [], (,), and -> (though the symmetry is imperfect for ->).
Furthermore, we need three function types / kinds to describe the three lambdas one level higher:
(4) the type of functions (5) the type of polymorphic values (6) the kind of type functions
In ghc, we already have "forall" for (5), and arrows for (4) and (6).
I would say that (3) is the "type-level abstraction", not (5).
I'm not sure I follow what you mean. Given the relationship between /\ and forall as demonstrated in the definition of id above, I don't see such a difference between #3 and #5. That is, given the need for #2 the need for #5 follows; from there #3 follows by extending the wording of #5. (Though #6 is desirable from a theoretical perspective I'm not sure whether the language needs to be able to express it. There's much else at the kind-layer we cannot express.) In other words, just because forall is the type of /\ doesn't mean that that's all it is. All of these are effectively identical: -- Just a type-level lambda five :: (forall a. a) Int five = 5 -- Making the term-level match the type exactly five :: (forall a. a) Int five = (/\a. 5::a) @Int -- Hiding a CAF behind a constant type -- (somewhat like how numeric constants really work) five :: Int five = (/\a. 5::a) @Int -- Boring five :: Int five = 5 -- Live well, ~wren
wren ng thornton wrote:
Thus, the forall keyword is serving as the type-level abstraction.
What do you mean by "type-level abstraction" here?
I mean an abstraction, as in a lambda-abstraction (aka a lambda-expression), at the type level.
[...]
I'm not sure I follow what you mean.
I mean that the forall keyword is *not* serving as the type-level abstraction. There is a difference between abstraction (as in lambda abstraction) and the type of abstractions (as in function types). In pure type systems, we have two different binders for these different features: - lower-case lambda for abstraction (on all levels) - upper-case Pi for the type of abstractions (on all levels) I find it highly confusing to say that forall denotes type-level abstraction, because it does not denote abstraction at all. It rather denotes the type of an abstraction, namely in Haskell, the type of abstracting over types in terms. In other words, the following is not legal Haskell, and not how forall works in any polymorphic lambda calculus:
-- Just a type-level lambda five :: (forall a. a) Int five = 5
-- Making the term-level match the type exactly five :: (forall a. a) Int five = (/\a. 5::a) @Int
Note that (forall a . a) has kind *, so (forall a . a) Int is not even well-kinded, as ghci correctly determines:
ghci -XRankNTypes :k (forall a. a) (forall a. a) :: *
:k (forall a . a) Int <interactive>:1:0: Kind error: `forall a. a' is applied to too many type arguments
About syntax:
(1) abstraction over terms in terms (to construct functions) (2) abstraction over types in terms (to construct polymorphic values) (3) abstraction over types in types (to construct type functions)
The syntax of #3 could also be conflated with the syntax of #2, for the same reason: they are in different syntactic categories. I pointed this out because the capital-lambda was the syntax others in the thread were using. Also, it makes sense to me to have #2 and #3 ("abstraction over types in _") paired together, rather than #1 and #3 ("abstraction over X in X"). Pairing #2/#3 also gives term/type symmetry as we have for other built-ins like [], (,), and -> (though the symmetry is imperfect for ->).
I agree that this makes as much sense as my view. However, I still argue that the existing type/kind symmetry for -> should be reflected in a term/type symmetry for \. We already have: id x = x type Id x = x :t id id :: a -> a :k Id Id :: * -> * And I think anonymous type-level abstraction should look like this: id' = \x -> x type Id' = \x -> x :t id' id' :: a -> a :k Id' Id' :: * -> * I would use the upper-case lambda for kind-polymorphism on the type level. type Id'' = /\k -> \t :: k -> t :k Id'' :: forall k . k -> k :k Id'' [*] :: * -> * :k Id'' [*] Int = Int :k Id'' [forall k . k -> k] Id'' [*] Int = Int Tillmann
Tillmann Rendel wrote:
wren ng thornton wrote:
Thus, the forall keyword is serving as the type-level abstraction.
What do you mean by "type-level abstraction" here?
I mean an abstraction, as in a lambda-abstraction (aka a lambda-expression), at the type level.
[...]
I'm not sure I follow what you mean.
I mean that the forall keyword is *not* serving as the type-level abstraction.
There is a difference between abstraction (as in lambda abstraction) and the type of abstractions (as in function types). In pure type systems, we have two different binders for these different features:
- lower-case lambda for abstraction (on all levels) - upper-case Pi for the type of abstractions (on all levels)
I find it highly confusing to say that forall denotes type-level abstraction, because it does not denote abstraction at all. It rather denotes the type of an abstraction, namely in Haskell, the type of abstracting over types in terms.
I view these as different sides of the same coin. There are two different senses of the "forall" keyword. There's the implicit Rank-1 quantifier, and then there's the Rank-N quantifier for polymorphic components. Your intuition is relying on the latter, whereas mine is relying on the former. The difference is similar to the difference between morphisms vs exponential objects in CCCs. We often find it convenient to elide the conversions between them, but they are in fact quite different. And if, at the term layer, functions can be silently lifted to/lowered from closures, then why not also at the type layer? While it is important to keep the ideas distinct, in practice we've found great utility in conflating the two faces of the coin. Why can't the type of abstractions be an abstraction of types? This is not currently the case in GHC, as you point out, but that does not demonstrate that the idea is unsound. This distributive transformation is used routinely in Conal Elliott's typeclass morphisms[1], Ralf Hinze's polyidiomatic lambda calculus[2], in HOAS (if you squint), and many other places where poly*ism spans multiple layers of the tower of interpretation. The symmetry between forall and /\ in System F is simply too great to write off without investigation. In any case, I think this discussion has veered far afield from the intent of my original footnote, which was simply to point out that the capital-lambda binder already has a canonical usage in System F (so we should not co-op it for type abstractions, without express intention). I have little invested in the current discussion, and the Cafe list doesn't really seem like the best venue to pursue it. If you have references you think would enlighten me, I'd happily pursue them. Otherwise, I think the best color for the bikeshed is purple :) [1] http://conal.net/blog/tag/type-class-morphism/ [2] http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8//26/slides/ralf.pdf -- Live well, ~wren
data X a b = X a b> instance Functor (X a) where fmap f (X a b) = X a (f b)
Yeah, that works just fine.
On Fri, Jul 17, 2009 at 1:14 PM, Petr Pudlak
Hi, I have probably a very simple question, but I wasn't able to figure it out myself.
Consider a two-parameter data type:
data X a b = X a b
If I want to make it a functor in the last type variable (b), I can just define
instance Functor (X a) where fmap f (X a b) = X a (f b)
But how do I write it if I want X to be a functor in its first type variable? Is that possible at all? Something like:
instance Functor ??? where fmap f (X a b) = X (f a) b
Thanks in advance, Petr _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (8)
-
David Menendez -
Geoffrey Marchant -
John Lask -
Petr Pudlak -
porges＠porg.es -
Stefan Holdermans -
Tillmann Rendel -
wren ng thornton