Radek: Možná že pro Tebe silně typové jazyky vhodnější jsou. Ale obecně praxe ukazuje, že jazyky s bohatým typovým systémem - a obzvlášt ty, které jsi vyjmenoval - jsou na vývoj drahé. Jestli je to způsobeno jejich "ukecaností", tím, že je je těžké zvládnout, kvalitě knihoven (což zas ale mluví o praktičnosti navrhovatelů jazyka) nebo prostě postavení hvězd se můžeme dohadovat. Ale přijde mi poněkud (rozuměj dost hodně :-)) namyšlené tvrdit, že ty zástupy programátorů co používá "netypové" jazyky jsou blbci, protože zbytečně programují v křápech, když tady existuje úžasný jazyk, který vyřeší všechny jejich potřeby a budou v něm psát pětkrát rychlejc. Asi to bude trochu jinak.
..pro praxi.... Ano, když budu potřebovat garantovat korektnost jazyka, tak sáhnu po teorii, která mi to umožní verifikovat. Já netvrdím, že Ta deduktivní teorie je nanic. Tvrdím, že se hodí k něčemu, ale k něčemu zas ne a tak není důvod ji cpát tam, kam se nehodí. Tzn. klidně udělám jazyk s programovacím typovým systémem, pak vezmu jí nejbližší deduktivní teorii a jí to ověřím a popř. návrh jazyka upravím... nebo můžu i postupovat opačně, vyjít z deduktivní teorie: ukazuje se ale, že PJ vzniklé "z praxe" jsou v praxi úspěšnější a tedy se dá s velkou jistotou říci, že užitečnější, než ty, které vzejdou z teorie...
...můžeme definovat sémantiku ... intersection and unions... A je to potřeba? Používá to nějaký jazyk, který je masivněji používán v praxi? Proč nahrazovat definici, která nám umožňuje zachycovat a klasifikovat to, co zachytit a klasifikovat potřebujeme, definicí, která nám nezachycuje to, co potřebujeme, ale zato umožní věc, kterou nepotřebujeme?
V pythonu máme typy. V C máme typy. Ty typy se něčím liší a něco mají společné. Úkol teoretika není přijít s teorií, která řekne: v Pythonu typy nejsou. Úkol teoretika je přijít a vymyslet teorii, která nejenže vystihne rozdíly, mezi těmi typy (to se té teorii povedlo dokonale :-)), ale také vystihne to, co mají tyto typy společného. Až přijdete s touto teorií, určitě ji bez problémů prosadíte...
Andy: Haskell umím natolik, že sem měl kdysi z jednosemestrový přednášky jedničku ;-) a od tý doby jsem ho asi neviděl. Takže moc ne :-) Ale jinak souhlasím, typový systém je dobrá věc a čím silnější, tím lepší - taky programuji spíš v "netypových" jazycích a dělám chyby, které by mě silně typový systém odchytil, jen co bych je napsal. Jenže - přesně jak píšeš - se za to něco platí. Někdy je to cena malá (pro velké aplikace se spíše hodí typově silné jazyky), někdy je ta cena příliš velká. A ta dělící čára nejde jen malé/velké aplikace. Ona jde i naskrz programovacíma metodikama: na agilní vývoj se hodí spíše "netypové" jazyky, zatímco silně typové jazyky se hodí spíš na tradiční vývojový cyklus atd... A i každému sedí něco jiného: někdo je roztržitý a tak ocení typovou kontrolu hodně, někdo je schopen psát "z první" a pak je s míň ukecaným jazykem (to jde většinou ruku v ruce) rychlejší.