abclinuxu.cz AbcLinuxu.cz itbiz.cz ITBiz.cz HDmag.cz HDmag.cz abcprace.cz AbcPráce.cz
AbcLinuxu hledá autory!
Inzerujte na AbcPráce.cz od 950 Kč
Rozšířené hledání
×
    včera 18:33 | IT novinky

    Nové verze AI modelů. Společnost OpenAI představila GPT‑5.5. Společnost DeepSeek představila DeepSeek V4.

    Ladislav Hagara | Komentářů: 0
    včera 15:33 | Zajímavý článek

    Nová čísla časopisů od nakladatelství Raspberry Pi zdarma ke čtení: Raspberry Pi Official Magazine 164 (pdf) a Hello World 29 (pdf).

    Ladislav Hagara | Komentářů: 0
    včera 04:44 | Komunita

    Bylo oznámeno, že webový prohlížeč Opera GX zaměřený na hráče počítačových her je už také na Flathubu and Snapcraftu.

    Ladislav Hagara | Komentářů: 0
    23.4. 23:11 | IT novinky

    Akcionáři americké mediální společnosti Warner Bros. Discovery dnes schválili převzetí firmy konkurentem Paramount Skydance za zhruba 110 miliard dolarů (téměř 2,3 bilionu Kč). Firmy se na spojení dohodly v únoru. O část společnosti Warner Bros. Discovery dříve usilovala rovněž streamovací platforma Netflix, se svou nabídkou však neuspěla. Transakci ještě budou schvalovat regulační orgány, a to nejen ve Spojených státech, ale také

    … více »
    Ladislav Hagara | Komentářů: 0
    23.4. 22:33 | Nová verze

    Canonical vydal (email, blog, YouTube) Ubuntu 26.04 LTS Resolute Raccoon. Přehled novinek v poznámkách k vydání. Vydány byly také oficiální deriváty Edubuntu, Kubuntu, Lubuntu, Ubuntu Budgie, Ubuntu Cinnamon, Ubuntu Kylin, Ubuntu Studio, Ubuntu Unity a Xubuntu. Jedná se o 11. vydání s dlouhodobou podporou (LTS).

    Ladislav Hagara | Komentářů: 2
    23.4. 11:55 | Nová verze

    V programovacím jazyce Go naprogramovaná webová aplikace pro spolupráci na zdrojových kódech pomocí gitu Gitea (Wikipedie) byla vydána v nové verzi 1.26.0. Přehled novinek v příspěvku na blogu.

    Ladislav Hagara | Komentářů: 0
    23.4. 04:44 | Pozvánky

    Ve středu 29. dubna 2026 se v pražské kanceláři SUSE v Karlíně uskuteční 7. Mobile Linux Hackday, komunitní setkání zaměřené na Linux na mobilních zařízeních, kernelový vývoj i uživatelský prostor. Akce proběhne od 10:00 do večerních hodin. Hackday je určen všem zájemcům o praktickou práci s Linuxem na telefonech. Zaměří se na vývoj aplikací v userspace, například bankovní aplikace, zpracování obrazu z kamery nebo práci s NFC, i na úpravy

    … více »
    lkocman | Komentářů: 1
    22.4. 21:55 | Nová verze

    LilyPond (Wikipedie) , tj. multiplatformní svobodný software určený pro sazbu notových zápisů, byl vydán ve verzi 2.26.0. Přehled novinek v aktualizované dokumentaci.

    Ladislav Hagara | Komentářů: 0
    22.4. 20:33 | Nová verze

    Byla vydána nová verze 11.0.0 otevřeného emulátoru procesorů a virtualizačního nástroje QEMU (Wikipedie). Přispělo 237 vývojářů. Provedeno bylo více než 2 500 commitů. Přehled úprav a nových vlastností v seznamu změn.

    Ladislav Hagara | Komentářů: 0
    22.4. 13:33 | IT novinky

    Společnost SpaceX amerického miliardáře Elona Muska oznámila, že si zajistila opci buď na akvizici startupu Cursor za 60 miliard dolarů (přes 1,2 bilionu Kč) do konce letošního roku, nebo na zaplacení deseti miliard dolarů za nové partnerství s touto firmou zabývající se generováním kódů. SpaceX se dále prosazuje na lukrativním trhu s vývojářskými nástroji pro umělou inteligenci (AI). Cursor, startup zabývající se prodejem modelů AI pro

    … více »
    Ladislav Hagara | Komentářů: 2
    Které desktopové prostředí na Linuxu používáte?
     (14%)
     (8%)
     (2%)
     (13%)
     (31%)
     (3%)
     (6%)
     (2%)
     (15%)
     (25%)
    Celkem 1408 hlasů
     Komentářů: 30, poslední 3.4. 20:20
    Rozcestník

    Administrace komentářů

    Jste na stránce určené pro řešení chyb a problémů týkajících se diskusí a komentářů. Můžete zde našim administrátorům reportovat špatně zařazenou či duplicitní diskusi, vulgární či osočující příspěvek a podobně. Děkujeme vám za vaši pomoc, více očí více vidí, společně můžeme udržet vysokou kvalitu AbcLinuxu.cz.

    Příspěvek
    8.2.2013 13:38 Radek Miček | skóre: 23 | blog: radekm_blog
    Rozbalit Rozbalit vše Re: Teorie programovani a "derivace funkce"
    Coq jsem se chtel naucit, ale zatim jsem na to nesebral odvahu.
    Až se odhodláte, tak doporučuji začít se Software Foundations a poté pokračovat Certified Programming with Dependent Types.
    ten zmineny clanek, akorat nejde stahnout
    Teď jsem to zkoušel a podařilo se to. Možná to chce jen správné načasování.
    Jenom moc nechapu, je opravdu nutne nejak deklarovat pro ta prepisovaci pravidla tu asociativitu (a tedy mit typovy system takto silny)
    Na přepisovací pravidla v GHC nejsou kladena žádná velká omezení. Je to čistě vaše věc, jestli pravidla zachovají význam programu nebo jestli přepisování vůbec skončí – nic z toho se nekontroluje.
    nebylo by mozne to proste rict, ze ta konkretni funkce vstupujici do toho reduce je asociativni (treba soucet)? Nedalo by se to prece jen nejak obejit?
    Pokud vám nevadí, že to nekontroluje kompilátor, tak dalo. Nejjednodušší je udělat dvě funkce reduce a reducePar, přičemž ta první není paralelní a nepotřebuje asociativitu, ta druhá je paralelní a potřebuje asociativitu (ale kompilátor o tom nic neví). Nebo mohu vyžadovat, aby datový typ byl instancí typové třídy, jenž má asociativní operaci a používat výhradně onu operaci:
    import Data.Monoid
    
    -- Funguje i s prazdnym seznamem, protoze monoid ma neutralni prvek.
    reduce :: Monoid a => [a] -> a
    reduce = mconcat
    
    A do třetice mohu napsat opět dvě varianty reduce – jednu pro obyčejné binární funkce a druhou pro asociativní (ve skutečnosti ta druhá není pro funkce, ale pro prvky typu Assoc a):
    {-# LANGUAGE TypeFamilies, FlexibleInstances #-}
    
    import qualified Debug.Trace as D
    
    class Reduction f where
        type El f
        reduce :: f -> [El f] -> El f
    
    instance Reduction (a -> a -> a) where
        type El (a -> a -> a) = a
        reduce = foldl1 . D.trace "normalni"
    
    newtype Assoc a = Assoc { unassoc :: (a -> a -> a) }
    
    instance Reduction (Assoc a) where
        type El (Assoc a) = a
        reduce = foldl1 . unassoc . D.trace "paralelni"
    
    Když pak v GHCi zavolám reduce (+) [1..5], tak dostanu výstup
    normalni
    15
    
    a když zavolám reduce (Assoc (+)) [1..5], tak dostanu výstup
    paralelni
    15
    
    Problém všech třech řešení je v tom, že kompilátor asociativitu nekontroluje, neboť ani neví, že daná funkce má být asociativní. Výhodou silnějších typových systémů je, že asociativitu nebo jinou vlastnost může ověřovat kompilátor.

    V tomto formuláři můžete formulovat svou stížnost ohledně příspěvku. Nejprve vyberte typ akce, kterou navrhujete provést s diskusí či příspěvkem. Potom do textového pole napište důvody, proč by měli admini provést vaši žádost, problém nemusí být patrný na první pohled. Odkaz na příspěvek bude přidán automaticky.

    Vaše jméno
    Váš email
    Typ požadavku
    Slovní popis
    ISSN 1214-1267   www.czech-server.cz
    © 1999-2015 Nitemedia s. r. o. Všechna práva vyhrazena.