a jste si jistý, že ten současný stav poznání máte podchycený? teď narážím na "dependent types"
Ano, jsem si tím jistý.
V různých dobách se perpetua mobile vytvářejí na základě v té době moderních věcí – někdy to byl „magnétismus“, někdy „paprsky X“, jindy „elektřina“, dneska to často budou „kvantové jevy“, „energie vakua“ nebo nejnověji nejspíš „temná hmota“. Což nic nemění na tom, že nemožnost konstrukce perpetua mobile plyne z fundamentálních zákonů, a nemusíme znát detailní fungování temné hmoty, nemusíme mít sjednocenou teorii gravitace a kvantové teorie, nemusíme tušit, co se ve fyzice objeví za padesát nebo za sto let, pořád si ale můžeme býti dost jistí, že ani pak nepůjde zkonstruovat perpetuum mobile.
Stejně tak si můžeme být dost jistí, že nepůjde mechanicky zkontrolovat, zda program bude fungovat správně – například i proto, že „správné fungování“ je subjektivní věc, a co může být v jednom případě považováno za správné fungování, v jiném případě tak být nemusí.
Pak je podstatná ještě jedna věc, která tu zatím moc nebyla zmíněna, a to je to, že typový systém může něco užitečného přinést jedině tehdy, když se používá, tedy když ho programátoři chtějí používat. Stačí se podívat na takové malinké vylepšení hloupého typového systému Javy, jakým jsou kontrolované výjimky. Ani tohle drobné typové omezení se prakticky neujalo, a to je velmi jednoduché kontrolované výjimky jak definovat, tak používat. I to připadá většině Java vývojářů jako zbytečně moc práce v porovnání s jejím přínosem. Takže navrhovat nové typy pro masové použití klidně můžete, ale pak se vám také klidně může stát, že budou vznikat a široce se používat knihovny, které budou jako jednu ze svých důležitých vlastností uvádět to, že ruší ten váš typový systém.
976 Odpovědí
128229 Zhlédnutí