Inzerujte na AbcPráce.cz od 950 Kč

napište » Zprávičky

sudo-rs nahradí v Ubuntu 25.10 klasické sudo

dnes 03:55 | Komunita

sudo-rs, tj. sudo a su přepsáné do programovacího jazyka Rust, nahradí v Ubuntu 25.10 klasické sudo. V plánu je také přechod od klasických coreutils k uutils coreutils napsaných v Rustu.

Ladislav Hagara | Komentářů: 1

Fedora oficiální distribucí WSL

včera 22:11 | Nasazení Linuxu

Fedora se stala oficiální distribucí WSL (Windows Subsystem for Linux).

Ladislav Hagara | Komentářů: 1

IBM LinuxONE Emperor 5

včera 13:22 | IT novinky

Společnost IBM představila server IBM LinuxONE Emperor 5 poháněný procesorem IBM Telum II.

Ladislav Hagara | Komentářů: 2

Lazarus 4.0

včera 04:55 | Nová verze

Byla vydána verze 4.0 multiplatformního integrovaného vývojového prostředí (IDE) pro rychlý vývoj aplikaci (RAD) ve Free Pascalu Lazarus (Wikipedie). Přehled novinek v poznámkách k vydání. Využíván je Free Pascal Compiler (FPC) 3.2.2.

Ladislav Hagara | Komentářů: 1

Kampaň Konec desítek (End of 10)

včera 00:33 | Komunita

Podpora Windows 10 končí 14. října 2025. Připravovaná kampaň Konec desítek (End of 10) může uživatelům pomoci s přechodem na Linux.

Ladislav Hagara | Komentářů: 28

Virtuální Bastlírna vol. 50: Power Over HDMI?

5.5. 23:22 | Pozvánky

Již tuto středu proběhne 50. Virtuální Bastlírna, tedy dle římského číslování L. Bude L značit velikost, tedy více diskutujících než obvykle, či délku, neboť díky svátku lze diskutovat dlouho do noci? Bude i příští Virtuální Bastlírna virtuální nebo reálná? Nejen to se dozvíte, když dorazíte na diskuzní večer o elektronice, softwaru, ale technice obecně, který si můžete představit jako virtuální posezení u piva spojené s učenou

… více »

bkralik | Komentářů: 1

Konec Skypu

5.5. 22:33 | IT novinky

Dle plánu dnes končí služba Skype. Uživatelé mohou pokračovat v Microsoft Teams.

Ladislav Hagara | Komentářů: 1

Statistický geoportál nově nabízí otevřená GIS data

5.5. 21:44 | IT novinky

Český statistický úřad rozšiřuje Statistický geoportál o Datový portál GIS s otevřenými geografickými daty. Ten umožňuje stahování datových sad podle potřeb uživatelů i jejich prohlížení v mapě a přináší nové možnosti v oblasti analýzy a využití statistických dat.

Ladislav Hagara | Komentářů: 2

Notový zápis v chytrých brýlích

5.5. 12:33 | Zajímavý projekt

Kevin Lin zkouší využívat chytré brýle Mentra při hraní na piano. Vytváří aplikaci AugmentedChords, pomocí které si do brýlí posílá notový zápis (YouTube). Uvnitř brýlí běží AugmentOS (GitHub), tj. open source operační systém pro chytré brýle.

Ladislav Hagara | Komentářů: 1

Jarní konference EurOpen.cz 2025

5.5. 12:11 | Pozvánky

Jarní konference EurOpen.cz 2025 proběhne 26. až 28. května v Brandýse nad Labem. Věnována je programovacím jazykům, vývoji softwaru a programovacím technikám.

Ladislav Hagara | Komentářů: 0

Centrum | Napsat | Starší

navrhněte » Anketa

Komentářů: 22, poslední 5.5. 10:06

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