Difficulty deriving a general type for combinator - comp.lang.haskell

Допис з розмови Difficulty deriving a general type for combinator

Dirk Thierbach

Переглянути профіль

Більше налаштувань 13 Вер 2008, 09:06

Групи новин: comp.lang.haskell

Від: Dirk Thierbach <dthierb...@usenet.arcornews.de>

Дата: Sat, 13 Sep 2008 08:06:08 +0200

Локально: Сб 13 Вер 2008 09:06

Тема: Re: Difficulty deriving a general type for combinator

  Відповісти автору
  |
  Переслати | Друкувати | Дивитися гілку
  | Показати оригінал
  | Повідомити адміністраторів про цей допис | Знайти повідлмлення від цього автора
  

Simon Richard Clarkstone <s.r.clarkst...@dunelm.org.uk> wrote:

> Suppose I have a set of functions like these:

> 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

Відповісти автору Переслати