Inzerujte na AbcPráce.cz od 950 Kč

napište » Zprávičky

Upozornění pro uživatele Asahi Linuxu: Neaktualizujte macOS na verzi 27 Golden Gate!

včera 22:22 | Komunita

Upozornění pro uživatele Asahi Linuxu: Neaktualizujte macOS na verzi 27 Golden Gate! Apple změnil detekci spouštěcích oddílů. Po aktualizaci oddíl s Asahi Linuxem nevidí. Snad je to jenom chyba.

Ladislav Hagara | Komentářů: 0

Prezentace a videa z Dne IPv6 jsou na webu akce

včera 15:11 | Komunita

Na webu konference Den IPv6, která se konala 4. června v Národní technické knihovně v pražských Dejvicích, jsou nyní k dispozici všechny prezentace (v PDF) a jejich videozáznamy. Organizátory konference byly i letos sdružení CESNET, CZ.NIC a NIX.CZ.

VSladek | Komentářů: 0

digiKam 9.1.0

včera 13:11 | Nová verze

Byla vydána nová verze 9.1.0 správce sbírky fotografií digiKam (Wikipedie). Přehled novinek i s náhledy v oficiálním oznámení (NEWS). Vypíchnout lze vylepšené vyhledávání nebo podporu Pixel Motion Photos. Nejnovější digiKam je ke stažení také jako balíček ve formátu AppImage. Stačí jej stáhnout, nastavit právo ke spuštění a spustit.

Ladislav Hagara | Komentářů: 0

Přihlaste přednášku na LinuxDays 2026

včera 11:44 | Pozvánky

Přihlaste svou přednášku na další ročník konference LinuxDays, který proběhne 3. a 4. října na FIT ČVUT v pražských Dejvicích. Příjem témat poběží do konce prázdnin, pak proběhne veřejné hlasování a následně sestavení programu.

Petr Krčmář | Komentářů: 2

Apache HTTP Server (httpd) 2.4.68 řeší 13 zranitelností

včera 04:44 | Nová verze

Byla vydána nová verze 2.4.68 svobodného multiplatformního webového serveru Apache (httpd). Řešeno je mimo jiné 13 zranitelností.

Ladislav Hagara | Komentářů: 2

WWDC26

8.6. 22:44 | IT novinky

Apple na své vývojářské konferenci WWDC26 (Worldwide Developers Conference, keynote) představil řadu novinek. Vypíchnout lze novou generaci Apple Intelligence a zbrusu novou Siri, která dostala název Siri AI. Kvůli Aktu o digitálních trzích (DMA) však funkce Siri AI nebudou v systémech iOS 27 a iPadOS 27 k dispozici uživatelům v Evropské unii.

Ladislav Hagara | Komentářů: 0

Flatpak 1.18.0

8.6. 22:22 | Nová verze

Byla vydána nová verze 1.18.0 distribučního frameworku Flatpak (Wikipedie), tj. technologie umožňující distribuovat aplikace v podobě jednoho instalačního souboru na různé linuxové distribuce a jejich různá vydání. Přehled novinek na GitHubu. Vypíchnout lze podporu rozhraní /dev/kfd pro výpočty na kartách AMD (AMDKFD).

Ladislav Hagara | Komentářů: 0

aMule 3.0.0

8.6. 20:44 | Nová verze

aMule (Wikipedie), tj. multiplatformní klient pro peer-to-peer sdílení souborů pro sítě eD2k and Kademlia, byl po více než pěti letech od vydání poslední verze 2.3.3, vydán v nové major verzi 3.0.0 (GitHub). S novou webovou stránkou a dokumentací.

Ladislav Hagara | Komentářů: 5

29. ročník IOCCC

8.6. 12:55 | IT novinky

Byly vyhlášeni vítězové a zveřejněny vítězné zdrojové kódy (YouTube, GitHub) již 29. ročníku soutěže International Obfuscated C Code Contest (IOCCC), tj. soutěže o nejnepřehlednější (nejobfuskovanější) zdrojový kód v jazyce C.

Ladislav Hagara | Komentářů: 0

Evropská komise předložila evropský balíček pro technologickou suverenitu

8.6. 12:44 | IT novinky

Evropská komise předložila evropský balíček pro technologickou suverenitu, tedy soubor opatření, která mají posílit kapacity EU v oblasti polovodičů, umělé inteligence, cloudu a open source. To Evropě pomůže stát se lídrem v oblasti umělé inteligence, posílit její digitální autonomii a vytvářet podmínky pro udržitelnější digitální budoucnost.

Ladislav Hagara | Komentářů: 15

Centrum | Napsat | Starší

navrhněte » Anketa

Komentářů: 30, poslední 3.4. 20:20

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.

Offtopic diskuse použijte pro diskusi mimo záběr našeho portálu (včelařství, windows), která by měla být smazána.
Duplicitní diskuse je určena pro případ, kdy uživatel odeslal svůj dotaz několikrát.
Návrh na cenzuru použijte, pokud komentář obsahuje urážky, vulgarismy nebo porušuje zákony.
Návrh na smazání komentáře je velmi neobvyklá akce používaná obvykle při nepovolené reklamě či spamu, výkřicích psychicky nemocných jedinců (ještírci) nebo pro smazání duplikátních komentářů.
Oprava formátování je žádost pro úpravu formy příspěvku, například pokud někdo píše bez odstavců nebo použije PRE pro celý komentář. Žádosti o změnu obsahu budou zamítnuty.

Vaše jméno
Váš email
Typ požadavku

Slovní popis