2app_id_maybe :: (forall a. a -> Maybe a) -> (b,c) -> (Maybe b,Maybe c) 2app_id_maybe f (x, y) = (f x, f y)
2app_maybe_id :: (forall a. Maybe a -> a) -> (Maybe b,Maybe c) -> (b,c) 2app_maybe_id f (x, y) = (f x, f y)
2app_id_list :: (forall a. a -> [a]) -> (b, c) -> ([b], [c]) 2app_id_list f (x, y) = (f x, f y)
2app_id_listlist :: (forall a. a -> [[a]]) -> (b, c) -> ([[b]], [[c]]) 2app_id_listlist f (x, y) = (f x, f y)
2app_list_id :: (forall a. [a] -> a) -> ([b], [c]) -> (b, c) 2app_list_id f (x, y) = (f x, f y)
Well, since their code are textually identical one should obviously unify them:
2app f (x, y) = (f x, f y)
But what type does it have? The inferred type is:
2app :: (a -> b) -> (a, a) -> (b, b)
But that isn't general enough, so I want to annotate the type. I can't figure out how to express it. I tried the following, but it didn't even parse:
app2 :: (tf1 :: * -> *, tf2 :: * -> *) => (forall a. tf1 a -> tf2 a) -> (tf1 b, tf1 c) -> (tf2 b, tf2 c)
tf1 and tf2 are "type functions" of kind * -> *, more general than just type constructors of type * -> *.
---
The worst bit is that this function is trivial to write in dynamically-typed languages:
(define (app2 f x) (cons (f (car x) (cdr x))))
def app2(f, x): y, z = x return f(y), f(z)
-- Simon Richard Clarkstone: s.r.cl?rkst...@dunelm.org.uk / s?m?n_cl?rkst...@yahoo.co.uk | My half-daughter went to the GMH riots | | But all I got was this stupid ¥-shirt. |
> 2app_id_maybe :: (forall a. a -> Maybe a) -> (b,c) -> (Maybe b,Maybe c) > 2app_id_maybe f (x, y) = (f x, f y)
> 2app_maybe_id :: (forall a. Maybe a -> a) -> (Maybe b,Maybe c) -> (b,c) > 2app_maybe_id f (x, y) = (f x, f y)
> 2app_id_list :: (forall a. a -> [a]) -> (b, c) -> ([b], [c]) > 2app_id_list f (x, y) = (f x, f y)
> 2app_id_listlist :: (forall a. a -> [[a]]) -> (b, c) -> ([[b]], [[c]]) > 2app_id_listlist f (x, y) = (f x, f y)
> 2app_list_id :: (forall a. [a] -> a) -> ([b], [c]) -> (b, c) > 2app_list_id f (x, y) = (f x, f y)
> Well, since their code are textually identical one should obviously > unify them:
> 2app f (x, y) = (f x, f y)
> But what type does it have? The inferred type is:
> 2app :: (a -> b) -> (a, a) -> (b, b)
> But that isn't general enough, so I want to annotate the type. I can't > figure out how to express it. I tried the following, but it didn't even > parse:
> app2 :: (tf1 :: * -> *, tf2 :: * -> *) => (forall a. tf1 a -> tf2 a) -> > (tf1 b, tf1 c) -> (tf2 b, tf2 c)
> tf1 and tf2 are "type functions" of kind * -> *, more general than just > type constructors of type * -> *.
That's more or less exactly what you need, though tf1 and tf2 cannot be predicates (typeclass related), but, as you say, must be "type functions". There's an extension of the typed lambda calculus called "System F" that allows such type functions. Unfortunately, it turns out that then a lot of decision problems about typing become undecidable, and also it is no longer guaranteed that every term can be assigned a most general type, so type inference goes out of the window.
For these reasons, Haskell is rather restricted compared to System F:
- It can infer only types without forall-quantifiers. - So if you need higher-rank forall-quantifiers, you have to annotate. - The only "type functions" in Haskell are datatype constructors. - It does allow forall-abstraction over types with higher kinds, so you could write
app2 :: forall tf1 tf2 b c. (forall a. tf1 a -> tf2 a) -> (tf1 b, tf1 c) -> (tf2 b, tf2 c)
And this would work for instances like
app2' :: (forall a. [a] -> Maybe a) -> ([b], [c]) -> (Maybe b, Maybe c)
but since "type functions" are restricted to constructors, there's no way to "write" a "identity type function", so your examples will fail. Similarly, because there's no way to write a "type function" that just drops its arguments and returns Int, instances like
app2' :: (Int -> Int) -> (Int, Int) -> (Int, Int)
will also fail. You can simulate all that to some degree by defining a new constructor, but then it will then have a slightly different type.
So with this example you have hit the spot where the Haskell type system just isn't expressive enough. In the literature, the function
twice f x = f (f x)
is the more famous example for the same phenomenon.
There are languages like Cayenne which implement full System F, but as described above, that means that they have to live with other disadvantages (like no or rather restricted type inference).
The good news is that this kind of problem happens *very* rarely in real world examples (I cannot remember a single time I've run into it).
Dirk Thierbach wrote: > Simon Richard Clarkstone <s.r.clarkst...@dunelm.org.uk> wrote: [...] >> Well, since their code are textually identical one should obviously >> unify them:
>> 2app f (x, y) = (f x, f y)
>> But what type does it have? The inferred type is:
>> 2app :: (a -> b) -> (a, a) -> (b, b)
>> But that isn't general enough, so I want to annotate the type. I can't >> figure out how to express it. I tried the following, but it didn't even >> parse: [...] > So with this example you have hit the spot where the Haskell type system > just isn't expressive enough. In the literature, the function
> twice f x = f (f x)
> is the more famous example for the same phenomenon.
> There are languages like Cayenne which implement full System F, but as > described above, that means that they have to live with other disadvantages > (like no or rather restricted type inference).
Well, these particular examples could both be typed if there were something like "union types". Using Java's syntax for interface unions:
app2 :: (a -> b && c -> d) -> (a,b) -> (c,d) twice :: (a -> b && b -> c) -> a -> c
One would not expect a compiler to infer that, but once annotated does it really muck up inference that much?
> The good news is that this kind of problem happens *very* rarely > in real world examples (I cannot remember a single time I've run into > it).
(whisper) Just don't let certain dynamic-types fans find out.
-- Simon Richard Clarkstone: s.r.cl?rkst...@dunelm.org.uk / s?m?n_cl?rkst...@yahoo.co.uk | My half-daughter went to the GMH riots | | But all I got was this stupid ¥-shirt. |
Будь ласка, поновіть своє прізвисько на сторінці налаштування передплати перед тим, як надіслати свій допис.
У вас немає права надсилання дописів до цієї групи.
Тему обговорення змінено на "Union/intersection types confusion (was: Re: Difficulty deriving a general type for combinator)" створено учасником Simon Richard Clarkstone
Simon Richard Clarkstone wrote: > Well, these particular examples could both be typed if there were > something like "union types". Using Java's syntax for interface unions:
> app2 :: (a -> b && c -> d) -> (a,b) -> (c,d) > twice :: (a -> b && b -> c) -> a -> c
I worded that very badly. "Type1 && Type2" in Java means an item from the intersection of the sets of items of each type, which AIUI is called an intersection type. When I said "union", I was thinking of the set of operations and contracts known to be present by examining the type: the union of the sets of method signatures of the two types.
Conversely, given a union type, the set of operations and contracts known to be present is the *intersection* of those for all the united types. I would guess there is a good reason for this reversal, and it is not just a coincidence.
-- Simon Richard Clarkstone: s.r.cl?rkst...@dunelm.org.uk / s?m?n_cl?rkst...@yahoo.co.uk | My half-daughter went to the GMH riots | | But all I got was this stupid ¥-shirt. |
Simon Richard Clarkstone <s.r.clarkst...@dunelm.org.uk> wrote:
> Dirk Thierbach wrote: >> There are languages like Cayenne which implement full System F, but as >> described above, that means that they have to live with other disadvantages >> (like no or rather restricted type inference). > Well, these particular examples could both be typed if there were > something like "union types".
It's been quite some time since I read papers about union types, so I cannot remember any details about their classification wrt. the other type systems, but I'm reasonably sure one could encode them into System F. So if there's a theorem that says you cannot have a most general type in System F for some terms, that means you'll run into the same sort of trouble even with union types, just for more complicated examples.
So in general, it won't work, and so far there's no real pressure to come up with a clever and more restricted scheme, because there have been no real examples so far where it would be really useful to have.
And I do remember vaguely that type inference with union types have some other difficulty (complexity?), that's probably why they haven't caught on.
>> The good news is that this kind of problem happens *very* rarely >> in real world examples (I cannot remember a single time I've run into >> it). > (whisper) Just don't let certain dynamic-types fans find out.
I'm sure they already found out; it's really old news. From my exposure to "certain dynamic-types fans" I think it's mostly a question of personality -- if their personality requires that the first solution that pops into their mind must run under all circumstances, then they should by all means use a dynamically typed language. They won't be happy with anything else, and nobody forces them to use something else. But then, for some reason "language fan" seems also to correlate with misinterpreting statements like "language X works for me, personally" from other people as "everybody must now drop the language they use and switch to language X". That makes discussions mostly futile :-(
Simon Richard Clarkstone <s.r.clarkst...@dunelm.org.uk> wrote: [...]
> app2 :: (a -> b && c -> d) -> (a,b) -> (c,d)
You probably meant (modulo alpha equivalence):
app2 :: (a -> c && b -> d) -> (a,b) -> (c,d)
The usual workaround for this particular typing problem in H-M languages is to pass two functions (or the same function twice with different types). IOW, you use a function with the following signature:
app2 :: (a -> c, b -> d) -> (a, b) -> (c, d)
> twice :: (a -> b && b -> c) -> a -> c
The same workaround can be used here too. Here is an example:
GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. Prelude> let twice (f, f') x = f' (f x) Prelude> :type twice twice :: (t -> t1, t1 -> t2) -> t -> t2 Prelude> let list x = [x] ; Prelude> :type list list :: t -> [t] Prelude> twice (list, list) () [[()]]
