Zkouška z funkcionálního programování

[zboj]

Protože v praktickém programování se FP nepoužívá...

Ani pro praktické programování v Haskellu to žádný důsledek nemá.

Něco by se asi našlo, třeba kompozice rozhodnutelné a nerozhodnutelné funkce může být rozhodnutelná, takže stojí za to se nad tím zamyslet a ujasnit si, kdy můžu bezpečně použít nerozhodnutelnou funkci (aniž by se mi výpočet zacyklil). Prostě obecně důsledky můžou být nepřímé a dalekosáhlé a své tvrzení bys těžko nějak rozumně obhájil (tvrzení o neexistenci se vyvrací snadno  )

[Reklama]

[JS]

Aha, dik. Ja jsem mel za to, ze o funkcich v "matematickem smyslu" se bavime uz v puvodnim prispevku. Asi by bylo lepe rikat tem Haskellovskym "castecne rekurzivni funkce".

[Mirek Prýmek]

Něco by se asi našlo, třeba kompozice rozhodnutelné a nerozhodnutelné funkce může být rozhodnutelná, takže stojí za to se nad tím zamyslet a ujasnit si, kdy můžu bezpečně použít nerozhodnutelnou funkci (aniž by se mi výpočet zacyklil). Prostě obecně důsledky můžou být nepřímé a dalekosáhlé a své tvrzení bys těžko nějak rozumně obhájil (tvrzení o neexistenci se vyvrací snadno  )

Tak to jsou důsledky práce s nerozhodnutelnými fcemi obecně. Já jsem myslel, že si moc neumím představit nějaké důsledky toho, že "monády nejsou monády [v matematickém smyslu]"

[zboj]

Aha, dik. Ja jsem mel za to, ze o funkcich v "matematickem smyslu" se bavime uz v puvodnim prispevku. Asi by bylo lepe rikat tem Haskellovskym "castecne rekurzivni funkce".

Jo, v té terminologii obecně je zmatek. Stěžejní je, co psal MP, naivní "řešení" si "nerozumí" s definicemi, tak se to různě obchází a v konečném důsledku beztak "no one cares", dokud nepadne na držku.

[zboj]

Něco by se asi našlo, třeba kompozice rozhodnutelné a nerozhodnutelné funkce může být rozhodnutelná, takže stojí za to se nad tím zamyslet a ujasnit si, kdy můžu bezpečně použít nerozhodnutelnou funkci (aniž by se mi výpočet zacyklil). Prostě obecně důsledky můžou být nepřímé a dalekosáhlé a své tvrzení bys těžko nějak rozumně obhájil (tvrzení o neexistenci se vyvrací snadno  )

Tak to jsou důsledky práce s nerozhodnutelnými fcemi obecně.

No jo, ale když haskellisti chtějí stavět na CT, tak nemůžou říct, že morfismy jsou jen rozhodnutelné funkce, protože když se dá nějaká RF rozložit na RF a narozhodnutelnou, tak v té kategorii pak jeden morfismus citelně chybí.

[Reklama]

[JS]

No jo, ale když haskellisti chtějí stavět na CT, tak nemůžou říct, že morfismy jsou jen rozhodnutelné funkce, protože když se dá nějaká RF rozložit na RF a narozhodnutelnou, tak v té kategorii pak jeden morfismus citelně chybí.

Tak ja to undefined beru jen jako takovou obezlicku, jak nechat program validne zkompilovat, kdyz mam rozepsany jen jeho kus.

Ale to co rikas se mi stejne moc nezda. Proc bychom nemohli uvazovat jen kategorii typu s RF? Ano, nebudou to vsechny funkce, ktere lze v Haskellu zapsat, ale jen ty totalni, ale to snad v praxi staci. Ze jde nejaka totalni rozlozit na parcialni nas pak prece nemusi trapit, to tu kategoricnost neohrozi.

[zboj]

No jo, ale když haskellisti chtějí stavět na CT, tak nemůžou říct, že morfismy jsou jen rozhodnutelné funkce, protože když se dá nějaká RF rozložit na RF a narozhodnutelnou, tak v té kategorii pak jeden morfismus citelně chybí.

Tak ja to undefined beru jen jako takovou obezlicku, jak nechat program validne zkompilovat, kdyz mam rozepsany jen jeho kus.

Ale to co rikas se mi stejne moc nezda. Proc bychom nemohli uvazovat jen kategorii typu s RF? Ano, nebudou to vsechny funkce, ktere lze v Haskellu zapsat, ale jen ty totalni, ale to snad v praxi staci. Ze jde nejaka totalni rozlozit na parcialni nas pak prece nemusi trapit, to tu kategoricnost neohrozi.

Když to chceš mít formálně přesně, tak to trápí. Když třeba nějaká funkce generuje polycyklické grupy a spojím ji s funkcí řešící word problem, tak dostanu hezkou vyčíslitelnou funkci, kterou chci logicky mít v Hask. Ono to má různé nuance a existují i jiná řešení, ale jsou koncepčně složitější.