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í
×
    dnes 04:11 | Komunita

    Fedora je od 10. února dostupná v Sýrii. Sýrie vypadla ze seznamu embargovaných zemí a Fedora Infrastructure Team mohl odblokovat syrské IP adresy.

    Ladislav Hagara | Komentářů: 9
    dnes 03:44 | Zajímavý projekt

    Ministerstvo zahraničí Spojených států amerických vyvíjí online portál Freedom.gov, který umožní nejenom uživatelům v Evropě přístup k obsahu blokovanému jejich vládami. Portál bude patrně obsahovat VPN funkci maskující uživatelský provoz tak, aby se jevil jako pocházející z USA. Projekt měl být původně představen již na letošní Mnichovské bezpečnostní konferenci, ale jeho spuštění bylo odloženo.

    NUKE GAZA! 🎆 | Komentářů: 3
    dnes 03:33 | Komunita

    Byla vydána pro lidi zdarma ke stažení kniha The Book of Remind věnovaná sofistikovanému kalendáři a připomínači Remind.

    Ladislav Hagara | Komentářů: 0
    včera 23:55 | Nová verze

    Grafický editor dokumentů LyX, založený na TeXu, byl vydán ve verzi 2.5.0. Oznámení připomíná 30. výročí vzniku projektu. Novinky zahrnují mj. vylepšení referencí nebo použití barev napříč aplikací, od rozhraní editoru po výstupní dokument.

    |🇵🇸 | Komentářů: 0
    včera 15:00 | Komunita

    F-Droid bannerem na svých stránkách a také v aplikacích F-Droid a F-Droid Basic upozorňuje na iniciativu Keep Android Open. Od září 2026 bude Android vyžadovat, aby všechny aplikace byly registrovány ověřenými vývojáři, aby mohly být nainstalovány na certifikovaných zařízeních Android. To ohrožuje alternativní obchody s aplikacemi jako F-Droid a možnost instalace aplikací mimo oficiální obchod (sideloading).

    Ladislav Hagara | Komentářů: 23
    20.2. 16:33 | Nová verze

    Svobodná historická realtimová strategie 0 A.D. (Wikipedie) byla vydána ve verzi 28 (0.28.0). Její kódový název je Boiorix. Představení novinek v poznámkách k vydání. Ke stažení také na Flathubu a Snapcraftu.

    Ladislav Hagara | Komentářů: 0
    20.2. 04:44 | Nová verze

    Multimediální server a user space API PipeWire (Wikipedie) poskytující PulseAudio, JACK, ALSA a GStreamer rozhraní byl vydán ve verzi 1.6.0 (Bluesky). Přehled novinek na GitLabu.

    Ladislav Hagara | Komentářů: 1
    20.2. 01:11 | Nová verze

    UBports, nadace a komunita kolem Ubuntu pro telefony a tablety Ubuntu Touch, vydala Ubuntu Touch 24.04-1.2 a 20.04 OTA-12.

    Ladislav Hagara | Komentářů: 0
    19.2. 18:00 | Nová verze

    Byla vydána (Mastodon, 𝕏) nová stabilní verze 2.0 otevřeného operačního systému pro chytré hodinky AsteroidOS (Wikipedie). Přehled novinek v oznámení o vydání a na YouTube.

    Ladislav Hagara | Komentářů: 1
    19.2. 16:00 | Zajímavý software

    WoWee je open-source klient pro MMORPG hru World of Warcraft, kompatibilní se základní verzí a rozšířeními The Burning Crusade a Wrath of the Lich King. Klient je napsaný v C++ a využívá vlastní OpenGL renderer, pro provoz vyžaduje modely, grafiku, hudbu, zvuky a další assety z originální kopie hry od Blizzardu. Zdrojový kód je na GitHubu, dostupný pod licencí MIT.

    NUKE GAZA! 🎆 | Komentářů: 9
    Které desktopové prostředí na Linuxu používáte?
     (18%)
     (6%)
     (0%)
     (11%)
     (27%)
     (2%)
     (5%)
     (2%)
     (12%)
     (26%)
    Celkem 931 hlasů
     Komentářů: 25, poslední 3.2. 19:50
    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.