Derivace typů

BigDataScientist

Derivace typů
« kdy: 06. 03. 2017, 11:27:22 »
Existuje nějaké intuitivní vysvětlení, proč "one hole context" (zipper) jde odvodit pomocí vzorečků pro derivace ze zápisu algebraického datového typu? Vysvětlení, proč to funguje na seznamech, stromech atd. mi přijde jednoduché, ale za boha nijak nemůžu pochopit, proč ty vzorečky vycházejí stejně jako v matematice pro spojité funkce, nevidím ani nejmenší konceptuální souvislost.


hu

Re:Derivace typů
« Odpověď #1 kdy: 06. 03. 2017, 12:03:05 »
Existuje nějaké intuitivní vysvětlení, proč "one hole context" (zipper) jde odvodit pomocí vzorečků pro derivace ze zápisu algebraického datového typu? Vysvětlení, proč to funguje na seznamech, stromech atd. mi přijde jednoduché, ale za boha nijak nemůžu pochopit, proč ty vzorečky vycházejí stejně jako v matematice pro spojité funkce, nevidím ani nejmenší konceptuální souvislost.

Mno, nebude to nejak souviset s timhle?

http://math.stackexchange.com/questions/135510/how-is-leibnizs-rule-for-the-derivative-of-a-product-related-to-the-binomial-fo

ava

Re:Derivace typů
« Odpověď #2 kdy: 06. 03. 2017, 12:10:32 »
Hmm, shledl jsem kdysi prednasku na tohle tema zde: http://2014.flatmap.no/speakers/pretty.html , ale nejsem teoretik a typum moc nerozumim, vic nemuzu slouzit :/

hu

Re:Derivace typů
« Odpověď #3 kdy: 06. 03. 2017, 12:12:06 »
Existuje nějaké intuitivní vysvětlení, proč "one hole context" (zipper) jde odvodit pomocí vzorečků pro derivace ze zápisu algebraického datového typu? Vysvětlení, proč to funguje na seznamech, stromech atd. mi přijde jednoduché, ale za boha nijak nemůžu pochopit, proč ty vzorečky vycházejí stejně jako v matematice pro spojité funkce, nevidím ani nejmenší konceptuální souvislost.

Mno, nebude to nejak souviset s timhle?

http://math.stackexchange.com/questions/135510/how-is-leibnizs-rule-for-the-derivative-of-a-product-related-to-the-binomial-fo

Jeste bych dodal, ze u one hole context se (co jsem videl) pracuje pouze s "derivacemi" polynomu, ktere lze s vyjimkou derivace linearni funkce a konstanty odvozovat rekurzivne prave pomoci Liebnizsova pravidla.

hu

Re:Derivace typů
« Odpověď #4 kdy: 06. 03. 2017, 12:24:35 »
Jeste bych dodal, ze u one hole context se (co jsem videl) pracuje pouze s "derivacemi" polynomu, ktere lze s vyjimkou derivace linearni funkce a konstanty odvozovat rekurzivne prave pomoci Liebnizsova pravidla.

s/polynomu/mocninnych fci

Berte to jenom jako hint, nemam ted cas se tim zabyvat a nikdy predtim jsem to nevidel. Ale jak jsou nekde stromy, binomicky koeficient se nabizi. Je proste mozne, ze ten koncept sdili algebraickou strukturu s okruhem s Liebniezovym pravidlem.

Podobne se pouzivaj v elektrice komplexni cisla pro reseni obvodu v harmonickem ustalenem stavu, ackoliv si asi neumite predstavit, co ma znamenat to "komplexni napeti".


andy

Re:Derivace typů
« Odpověď #5 kdy: 06. 03. 2017, 13:49:33 »

zboj

  • *****
  • 1 507
    • Zobrazit profil
    • E-mail
Re:Derivace typů
« Odpověď #6 kdy: 06. 03. 2017, 16:09:13 »
Existuje nějaké intuitivní vysvětlení, proč "one hole context" (zipper) jde odvodit pomocí vzorečků pro derivace ze zápisu algebraického datového typu? Vysvětlení, proč to funguje na seznamech, stromech atd. mi přijde jednoduché, ale za boha nijak nemůžu pochopit, proč ty vzorečky vycházejí stejně jako v matematice pro spojité funkce, nevidím ani nejmenší konceptuální souvislost.
Pozor na terminologii, zipper není one hole context (ale obsahuje ho).

Vysvětlení existuje matematické, algebraické typy tvoří polookruh, takže se na nich můžeme vyřádit včetně derivací. To ale není intuitivní vysvětlení.

Intuitivně derivace popisuje funkci v konkrétním bodě. Je-li derivace například lineární, udává úhel, jakým funkce určitým bodem probíhá, ale už neříká, jak se chová jinde, byť "hodně" blízko. One hole context popisuje algebraický datový typ v konkrétním bodě (konfiguraci), ale už neříká, jak vypadá, když se o kousek posunu. Úplně polopaticky: Když traktor jezdí náhodně, ale s velkým poloměrem zatáčení po velkém poli, tak v mlze uvidím jeho trasu jen jako přímku a pokud mám kompas, můžu určit úhel, jakým se pohyboval. Když si stoupnu doprostřed spojového seznamu, tak uvidím jeden seznam před sebou a jeden za sebou, tedy dva seznamy. Akorát si stojím na aktuálním prvku, tj. nevidím ho (to je ta "díra"). Když k tomuto "kontextu" ten prvek přidám, dostanu zipper.

Jinak intuitivně to je kostrbaté, protože funkce jako takové se uvažují ve spojitém prostoru, kdežto algebraické typy jsou diskrétní. Dá se to taky představit tak, že ten spojitý prostoru kvantizuju, podobně jako když ve hrách s každým krokem (FPS) upravit pózy agentů a objektů krokově podle derivace. Pak je ta souvislost názornější.

v

Re:Derivace typů
« Odpověď #7 kdy: 06. 03. 2017, 16:27:29 »