Fórum Root.cz

Hlavní témata => Vývoj => Téma založeno: Coati 03. 03. 2022, 23:12:12

Název: Ověření pravidel pro funktory
Přispěvatel: Coati 03. 03. 2022, 23:12:12
Ve funkcionálním programování se uvádí, že typové operátory musí splňovat několik rovností, aby byly funktory (viz například Wikipedie nebo dokumentace k Haskellu). Zároveň se uvádí, že programátor musí věřit autorům knihovny, že jejich funktory ony rovnosti splňují, že to překladač Haskellu neumí. Existuje nějaký jazyk, který umí podmínky u funktorů a podobných operátorů zaručit automaticky ve vší obecnosti?
Název: Re:Ověření pravidel pro funktory
Přispěvatel: waldir 04. 03. 2022, 12:31:15
Obecně ne, protože problém rovnosti turingovo strojů není rozhodnutelný.

Pro slabší nástroje podobného typu lze hledat klíčová slova:


Jinak samotné podmínky funktoru nejsou nijak složité a není důvod v nich knihovnám nevěřit. Hlavní problém je vyjádřit je tak aby se daly ověřit nad libovolným funktorem, protože pokud bychom dokázali genericky vyjádřit danou podmínku, pak bychom pravděpodobně dokázali sestavit plně generický funktor a vůbec nepotřebovali různé knihovní implementace.
Název: Re:Ověření pravidel pro funktory
Přispěvatel: Idris 04. 03. 2022, 14:54:13
samotné podmínky funktoru nejsou nijak složité a není důvod v nich knihovnám nevěřit
  ;D ;D ;D ;D ;D ;D ;D ;D ;D ;D

 ::)
Název: Re:Ověření pravidel pro funktory
Přispěvatel: Idris 04. 03. 2022, 15:08:28
  • "programming by contract"
  • "symbolic evaluation"
(b) je správně (zbytek příspěvku je blábol). V podstatě se jedná o jednoduché cvičení z úvodního kurzu do Agdy nebo Coqu, pro různé typy funktorů se dají podmínky symbolicky ověřit ("formálně verifikovat") poměrně snadno (i třeba flatMap apod., kde to je ale o chlup složitější). V případě Haskellu (ten původní nemá dostatečně silný typový systém, i když nějaká použitelná rozšíření už existují) se musí to ověření napsat v nějakém podobném funkcionálním jazyce, kde to ověřit jde, a pak ověřený kód podstrčit Haskellu.

BoneFlute se toho možná chytne a napíše si to ověření v rámci sebevzdělávání (a snad se pak s námi podělí o výsledek) :)