Ověření pravidel pro funktory

[Coati]

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?

[Reklama]

[waldir]

Obecně ne, protože problém rovnosti turingovo strojů není rozhodnutelný.

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

• "programming by contract" - což ale efektivně vede jen na různé formy assertů, kde co umíš upočítat to umíš ověřit. Obecnou ekvivalenci nad nekonečnou doménou ale neupočítáš.
• "symbolic evaluation" - neb jsou jazyky kde:
  
  • funkce jsou first-class objekty ve smyslu že funkce je možné nejen genericky tvořit a předávat, ale i (zpětně) číst a editovat (třeba lisp)
  • výrazy je možné vyhodnocovat i částečně, protože vše je jen symbol, a tedy s výrazy lze velmi flexibilně manipulovat včetně změn pořadí vyhodnocování, což z hlediska dokazování přeci jen dává člověku do ruky určité nástroje. (třeba mathematica)
    

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.

[Idris]

samotné podmínky funktoru nejsou nijak složité a není důvod v nich knihovnám nevěřit

 

 

[Idris]

• "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)