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

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

Dirk Thierbach

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

Більше налаштувань 20 Вер 2008, 01:43

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

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

Дата: Sat, 20 Sep 2008 00:43:57 +0200

Локально: Сб 20 Вер 2008 01:43

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

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

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 :-(

- Dirk

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