Fórum Root.cz
Práce => Studium a uplatnění => Téma založeno: desprit 22. 06. 2017, 06:52:34
-
Čeká mě zkouška z funkcionálního programování a kámoš právě vyletěl, když jako definici kategorie typů uvedl "objekty jsou typy a šipky jsou funkce mezi nimi". Nedostal se ani k důkazu, že definice má smysl. Mi to přijde správně, zjevně je v tom nějaký háček, víte někdo správnou odpověď?
-
Je to věcně správně. Pan učitel si možná potrpí na formálnější onanii, nemá rád slovo "šipka" a vyžaduje "morfismus" ;)
P.S. Na jaké je to škole, že se v rámci FP učí CT? Nebo je to nějaký pokročilý předmět z FP?
-
Je to věcně správně. Pan učitel si možná potrpí na formálnější onanii, nemá rád slovo "šipka" a vyžaduje "morfismus" ;)
I ty, Brute? Nope, je to věcně špatně a pan učitel si asi potrpí jen na přesnost (jaký to div ve světě matematiky). Morfismy (šipky se říká běžně, to problém není) nejsou všechny funkce, ale jen ty vyčíslitelné. Kdyby se braly v úvahu všechny, tak by to už nebyla kategorie (a taky to v FP nemá smysl).
Akorát teda nevím, jestli to je hned na vyhození, "kámoš" asi řekl ještě další kraviny nebo se hádal, že slůvko sem slůvko tam nehraje roli. Kolega takhle jednou vyhodil studenta, který tvrdil, že logika řádu n>=2 je neúplná, přičemž stačilo upřesnit formulaci, ale pako student se začalo hádat... :D
-
(šipky se říká běžně, to problém není)
Arrow je v Haskellu něco jinýho, proto by mu to teoreticky mohlo vadit, kdyby si chtěl na studentovi honit triko.
nejsou všechny funkce, ale jen ty vyčíslitelné. Kdyby se braly v úvahu všechny, tak by to už nebyla kategorie (a taky to v FP nemá smysl).
Že by ho vyhodil na takovou kravinu? No, jestli je debil, nebo jestli student dělal chytrýho, tak je to možný.
-
nejsou všechny funkce, ale jen ty vyčíslitelné. Kdyby se braly v úvahu všechny, tak by to už nebyla kategorie (a taky to v FP nemá smysl).
Že by ho vyhodil na takovou kravinu? No, jestli je debil, nebo jestli student dělal chytrýho, tak je to možný.
Toto rozlišení je celkem podstatné a v definici Hask se běžně nějaká ekvivalentní formulace uvádí. Funkce i jen z N do N můžou být docela svině.
-
Kdyby se braly v úvahu všechny, tak by to už nebyla kategorie
To mi nejak neni jasny, muzes to vysvetlit? Axiomy kategorie (tranzitivita a identita) to, zda se mi, splnuje.
-
Kdyby se braly v úvahu všechny, tak by to už nebyla kategorie
To mi nejak neni jasny, muzes to vysvetlit? Axiomy kategorie (tranzitivita a identita) to, zda se mi, splnuje.
možná tohle http://math.andrej.com/2016/08/06/hask-is-not-a-category/
-
Kdyby se braly v úvahu všechny, tak by to už nebyla kategorie
To mi nejak neni jasny, muzes to vysvetlit? Axiomy kategorie (tranzitivita a identita) to, zda se mi, splnuje.
Když třeba v Haskellu budu uvažovat i funkce, co ne vždy ukončí výpočet, tak na nich nejde rozumně nadefinovat ekvivalence (viz nedávná diskuze zde o ekvivalenci v JS), takže pak nedávají smysl třeba komutativní diagramy a veškeré definice ztrácí smysl.
-
Když třeba v Haskellu budu uvažovat i funkce, co ne vždy ukončí výpočet, tak na nich nejde rozumně nadefinovat ekvivalence (viz nedávná diskuze zde o ekvivalenci v JS), takže pak nedávají smysl třeba komutativní diagramy a veškeré definice ztrácí smysl.
Dalo by se to asi říct i jednodušeji neformálně: pokud je funkce z Int do bottom, tak bys musel mít typ bottom, ale na něm nejde udělat identita.
-
Když třeba v Haskellu budu uvažovat i funkce, co ne vždy ukončí výpočet, tak na nich nejde rozumně nadefinovat ekvivalence (viz nedávná diskuze zde o ekvivalenci v JS), takže pak nedávají smysl třeba komutativní diagramy a veškeré definice ztrácí smysl.
Dalo by se to asi říct i jednodušeji neformálně: pokud je funkce z Int do bottom, tak bys musel mít typ bottom, ale na něm nejde udělat identita.
Jo, to sis teď našel :P Prostě to kvůli tomuto nebude kategorie. IMHO je lepší uvažovat jen funkce v matematickém smyslu, je to stejný rozdíl jako třeba svaz všech podmnožin nějakého X a svaz všech konstruovatelných podmnožin, je to nějaká slušně se chovající algebraická struktura a že má nějaké relativně hnusné množiny navíc mě zajímat moc nemusí. Ostatně třeba u modelu ZFC mi je tak fuk, jestli je spočetný...
-
Jo, to sis teď našel :P
Naopak, teprve jak jsem to napsal, tak jsem klikl na ten link výš a uzarděl se, že jdu s dřívím do lesa ;)
-
Jo, to sis teď našel :P
Naopak, teprve jak jsem to napsal, tak jsem klikl na ten link výš a uzarděl se, že jdu s dřívím do lesa ;)
Každopádně jde o docel zajímavý vhled, ne? Jedním z důsledků například je, že monády ve FP nejsou monády :)
-
Každopádně jde o docel zajímavý vhled, ne? Jedním z důsledků například je, že monády ve FP nejsou monády :)
Ani ne, důsledky pro praktické programování to nemá žádné.
-
Každopádně jde o docel zajímavý vhled, ne? Jedním z důsledků například je, že monády ve FP nejsou monády :)
Ani ne, důsledky pro praktické programování to nemá žádné.
Protože v praktickém programování se FP nepoužívá...
-
Protože v praktickém programování se FP nepoužívá...
Ani pro praktické programování v Haskellu to žádný důsledek nemá.
-
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 :P)
-
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".
-
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 :P)
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]"
-
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.
-
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 :P)
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í.
-
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.
-
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ší.