• úvod
  • témata
  • události
  • tržiště
  • diskuze
  • nástěnka
  • přihlásit
    registrace
    ztracené heslo?
    LUDWIG_Funkcionální programování (Haskell, LISP, XQuery, OCaml, F#, Scala, ...) - praxe, teorie a uplatnění
    BROUKOID
    BROUKOID --- ---
    LITTLELI: co konkretne se ti na tom nelibi? Ze to nema podlozene nejakou studii?
    LITTLELI
    LITTLELI --- ---
    LUDWIG_: no škoda, že předposlední odstavec je spíš zbožné přání autora než nějaká forma ověřeného faktu
    LUDWIG_
    LUDWIG_ --- ---
    Pozvánka na Prague Lambda Meetup - Root.cz
    http://www.root.cz/zpravicky/pozvanka-na-prague-lambda-meetup/
    LUDWIG_
    LUDWIG_ --- ---
    LISKNI_SI
    LISKNI_SI --- ---
    IRAVEN: To fakt obecně nejde, protože taková funkce není vyčíslitelná. Představ si, že ta vstupní "množina" jsou právě všechny dvojice turingův stroj a jeho akceptující běh (tj. ta fce A → bool ověřuje, zda je to korektní zadání a zda to je skutečně akceptující běh toho stroje) a že ta transformace z toho vymaže ten běh (tj. tu dvojici transformuje jenom na to zadání turingova stroje). Tohle obojí jsou vyčíslitelné funkce, ale výsledkem té funkce by měla být množina všech turingových strojů, které zastaví. A ta rozhodně vyčíslitelná není.
    IRAVEN
    IRAVEN --- ---
    Upřesním :). Mám definovaný datový typ "množina", který je daný pouze jako funkce A -> bool, která říká TRUE právě když prvek A do množiny patří. Potom mám funkci A -> A, která mi převádí prvky na jiné prvky, například násobí dvěma. No a cílem je napsat funkci, která vrací "množinu" (čili funkci A -> bool) která obsahuje prvky ze zadaná množiny transformované zadanou funkcí (je to funkce vyššího řádu).

    Bavil jsem se o tom s kamarádem a došli jsme k tomu, že to zřejmě nejde bez nějaké iterace nad množinou (je potřeba cosi jako "exists").
    KAMAHL
    KAMAHL --- ---
    IRAVEN: Moc nechápu zadání, nemohl bys dát příklady vstupu a požadovaného výstupu?
    LUDWIG_
    LUDWIG_ --- ---
    IRAVEN: "zda A do mnoziny patri" = typ A patri do mnoziny ruznych typu, nebo parametr :: A patri do mnoziny hodnot typu A?
    LISKNI_SI
    LISKNI_SI --- ---
    IRAVEN: Jakože (. filter) . (.) . map? (Má to ty parametry opačně.)
    IRAVEN
    IRAVEN --- ---
    jak byste napsali funkci map, ktera ma na vstupu tyto parametry: funkce A -> bool ktera rika, zda A do mnoziny patri, a A -> B pro transformaci? a jde to vubec? mne prijde, ze bez inverzu B -> A ne...
    LITTLELI
    LITTLELI --- ---
    LUDWIG_: jak už jsem tu psal, tohle typový peklo mi přijde naprosto nadbytečný
    LUDWIG_
    LUDWIG_ --- ---
    LITTLELI: proc?
    LITTLELI
    LITTLELI --- ---
    LUDWIG_: tohle je děsivý :)
    LUDWIG_
    LUDWIG_ --- ---
    Functional Programming is Terrible
    https://www.youtube.com/watch?v=hzf3hTUKk8U
    GARFIELD
    GARFIELD --- ---
    IRAVEN: Dik za info, ale ted uz jsem mimo CR
    IRAVEN
    IRAVEN --- ---
    GARFIELD: myslim, ze v et netera hledaji scalisty
    KAMAHL
    KAMAHL --- ---
    Kdyby to někoho zajímalo, bylo mi na Coq doporučeno http://www.cis.upenn.edu/~bcpierce/sf/ a http://adam.chlipala.net/cpdt/ ale ještě jsem se do toho pořádně nedíval, nechám si to tu jako poznámku pro sebe :D
    LUDWIG_
    LUDWIG_ --- ---
    KAMAHL: pokud ciste "dependent types", tak Agda ci Idris bude asi lepsi volba: [ LUDWIG_ @ Funkcionální programování (Haskell, LISP, XQuery, OCaml, F#, Scala, ...) - praxe, teorie a uplatnění ]

    Idris je prakticky programovaci jazyk, zatimco Coq a Agda jsou spis pomocny software pro matematicke dukazy :)
    Jinak tady je kdyztak nova prednaska o Idrisu:
    Edwin Brady - Idris: Programming with Dependent Types
    http://vimeo.com/83665028
    KAMAHL
    KAMAHL --- ---
    Inspiroval mě tenhle článek http://blog.ezyang.com/2014/03/haskell-for-coq-programmers/ ale chtěl bych to naopak :D
    Kliknutím sem můžete změnit nastavení reklam