abclinuxu.cz AbcLinuxu.cz itbiz.cz ITBiz.cz HDmag.cz HDmag.cz abcprace.cz AbcPráce.cz
Inzerujte na AbcPráce.cz od 950 Kč
Rozšířené hledání
Přihlášení | Registrace
×
napište » Zprávičky
inzerujte » Pracovní nabídky
    Armbian 24.5.1 Havier
    včera 21:22 | Nová verze

    Armbian, tj. linuxová distribuce založená na Debianu a Ubuntu optimalizovaná pro jednodeskové počítače na platformě ARM a RISC-V, ke stažení ale také pro Intel a AMD, byl vydán ve verzi 24.5.1 Havier. Přehled novinek v Changelogu.

    Ladislav Hagara | Komentářů: 0
    Společnost xAI získala investici 6 miliard dolarů
    včera 19:44 | IT novinky

    Společnost xAI založena Elonem Muskem a stojící za AI LLM modelem Grok získala investici 6 miliard dolarů.

    Ladislav Hagara | Komentářů: 1
    Nový rekord NIX.CZ: 3,14 Tbps
    včera 15:44 | IT novinky

    Finálový zápas mistrovství světa v ledním hokeji přinesl nový rekord NIX.CZ (𝕏): "Dosavadní absolutní maximum našeho propojovacího uzlu bylo překonáno v čase 21:10, kdy jsme při přenosu dat dosáhli 3,14 Tbps. Je třeba také doplnit, že po deváté hodině večerní byly na maximu i ostatní datové přenosy nesouvisející s hokejovým šampionátem".

    Ladislav Hagara | Komentářů: 2
    Přihlaste přednášku na LinuxDays 2024
    včera 15:11 | Pozvánky

    Přihlaste svou přednášku na další ročník konference LinuxDays, který proběhne 12. a 13. října na FIT ČVUT v pražských Dejvicích. CfP poběží do konce prázdnin, pak proběhne veřejné hlasování a výběr přednášek.

    Petr Krčmář | Komentářů: 0
    HealthyPi Move, open source biometrický monitor ve tvaru hodinek
    25.5. 19:00 | Zajímavý projekt

    Na crowdsourcingové platformě Crowd Supply byla spuštěna kampaň na podporu open source biometrického monitoru ve tvaru hodinek HealthyPi Move. Cena je 249 dolarů a plánovaný termín dodání listopad letošního roku.

    Ladislav Hagara | Komentářů: 13
    ICQ přestane 26. června fungovat
    24.5. 22:22 | Upozornění

    ICQ přestane 26. června fungovat.

    Ladislav Hagara | Komentářů: 21
    Murena /e/OS 2.0
    24.5. 17:44 | Nová verze

    Firma Murena představila /e/OS verze 2.0. Jde o  alternativní sestavení Androidu bez aplikací Google. Mezi novinkami je podrobnější nastavení ochrany soukromí před sledováním aplikacemi. Murena prodává několik smartphonů s předinstalovaným /e/OS (Fairphone, repasovaný Google Pixel 5).

    Fluttershy, yay! | Komentářů: 0
    Hra zdarma: Warhammer 40,000: Gladius - Relics of War
    24.5. 14:33 | Zajímavý software

    Do 30. května lze v rámci akce Warhammer Skulls 2024 získat na Steamu zdarma hru Warhammer 40,000: Gladius - Relics of War.

    Ladislav Hagara | Komentářů: 1
    HelenOS 0.14.1
    24.5. 13:33 | Nová verze

    HelenOS (Wikipedie), tj. svobodný operační systém českého původu založený na architektuře mikrojádra, byl vydán ve verzi 0.14.1. Přehled novinek v poznámkách k vydání. Vypíchnou lze nabídku Start. Videopředstavení na YouTube.

    Ladislav Hagara | Komentářů: 3
    BreadboardOS pro Raspberry Pi Pico (RP2040)
    23.5. 23:22 | Zajímavý software

    BreadboardOS je firmware pro Raspberry Pi Pico (RP2040) umožňující s tímto MCU komunikovat pomocí řádkového rozhraní (CLI). Využívá FreeRTOS a Microshell.

    Ladislav Hagara | Komentářů: 0
    Centrum | Napsat | Starší
    navrhněte » Anketa
    Podle hypotézy Mrtvý Internet mj. tvoří většinu online interakcí boti.
     (89%)
     (3%)
     (4%)
     (4%)
    Celkem 915 hlasů
     Komentářů: 16, poslední 14.5. 11:05
    Rozcestník
    AbcLinuxu
    HDmag.cz

    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
    Píšeme jinde
    ISSN 1214-1267   www.czech-server.cz
    Redakce | Inzerce | Podmínky použití | Osobní údaje
    © 1999-2015 Nitemedia s. r. o. Všechna práva vyhrazena.