Haskell saját adattípussal segítség
2021-11-16T19:39:15+01:00
2021-11-19T19:01:47+01:00
2022-08-12T05:45:29+02:00
teki19
Eddig eljutottam a feladat megoldásában, de elakadtam. Tudna valaki segítnei?

Adjuk meg azt a függvényt, ami egy háttértár listából visszaadja az összes olyan HDD-t, aminek nagyobb a kapacítása, mint a legnagyobb kapacítású SSD-nek. A feladat megoldásához érdemes segényfüggvényt használni.

<

data Storage = HDD String Int Int | SSD String Int deriving (Show, Eq) capacity :: Storage -> Int capacity ( HDD _ a b )= b capacity ( SSD _ c)= c isHDD :: Storage -> Bool isHDD ( HDD a b c ) = True isHDD ( SSD a b ) = False maxcapacity :: [Srorage] -> Int maxcapacity (capacity x:capacity xs) | (capacity xs) > capacity x = maxcapacity | otherwise= capacity x hugeHDDs :: [Storage] -> [Storage] hugeHDDs []= [] where isHDD == False && capacity Tesztesetek, amiknek True-t kell visszadniuk: -- hugeHDDs [] == [] -- hugeHDDs [HDD "Seagate" 5600 250, HDD "Verbatim" 7200 1000, SSD "Samsung" 500, SSD "Samsung" 750] == [HDD "Verbatim" 7200 1000] -- hugeHDDs [HDD "Seagate" 5600 250, HDD "Verbatim" 7200 100, SSD "Samsung" 250, SSD "Samsung" 100] == [] -- hugeHDDs [HDD "Seagate" 5600 1000, HDD "Verbatim" 7200 1500, SSD "Samsung" 250, SSD "Samsung" 500] == [HDD "Seagate" 5600 1000,HDD "Verbatim" 7200 1500]
Mutasd a teljes hozzászólást!
A feladatot többféle stílusban is le lehet programozni.
A mellékelt fájlban szándékosan olyan stílust használok, ami kicsit műviesen mesterkélten konkrét, nem használ segédfüggvényeket, absztrakciókat, és hű marad az eredeti mintához.
Nem használom a szokásos optimalizálásokat sem, így elvileg egy-két dolgot duplán számol.
Mutasd a teljes hozzászólást!
Csatolt állomány

  • Az elso problema itt van:

    maxcapacity (capacity x: capacity xs)
    Nem lehet fuggvenyt a pattern match-en belul meghivni(legalabb is nem igy, hanem view pattern-ekkel)

    Aztan itt:

    (capacity xs) > capacity x = maxcapacity
    nem adsz parametert a maxcapacity-nek.

    Aztan van ez a sor:

    where isHDD == False && capacity
    Ez sok sebbol verzik. A where clause-ban fuggvenyeket definialhatsz de ez itt csak egy bool tipusu kifejezes. Masreszt a capacity fuggvenyt parameter nelkul hivod.

    Amugy amit en csinalnek(ha teljesitmeny nem szamit):
    1. filtereznem a kapott tarolokat, hogy csak az ssd-k maradjanak
    2. megneznem melyik a legnagyobb(maximumBy)
    3. filtereznem a kapott tarolokat megint ugy, hogy most csak a hdd-k maradjanak es csak azok amik nagyobbak a 2-es pontban megkapott max ssd meretnel.
    Mutasd a teljes hozzászólást!
  • A feladatot többféle stílusban is le lehet programozni.
    A mellékelt fájlban szándékosan olyan stílust használok, ami kicsit műviesen mesterkélten konkrét, nem használ segédfüggvényeket, absztrakciókat, és hű marad az eredeti mintához.
    Nem használom a szokásos optimalizálásokat sem, így elvileg egy-két dolgot duplán számol.
    Mutasd a teljes hozzászólást!
    Csatolt állomány
  • Mellékelem a második verziót.
    Itt szintén kerültöm a külön segédfüggvények, magasabb rendű függvények bevezetését, de elkerülöm a kifejezések ismétlését, újraszámítását afféle ,,segédváltozók''  (valójában a tisztán funkcionális let.. in... szerkezet) használatával.
    Mutasd a teljes hozzászólást!
    Csatolt állomány
  • Egyik megoldasod sem mukodik helyesen. Nem a legnagyobb ssd-nel nagyobb elemeket adod vissza hanem a 999-nel nagyobb meretueket szoval ez pl nem lesz igaz:

    hugeHDDs [HDD "Seagate" 5600 600, HDD "Verbatim" 7200 1500, SSD "Samsung" 250, SSD "Samsung" 500] == [HDD "Seagate" 5600 600,HDD "Verbatim" 7200 1500]
    A maxcapacity-t raadasul megirtad ket kulonbozo modon de egyiket sem hasznalod.

    Amugy nem ertem miert is akarnad megirni helyette, ugy semmit nem fog tanulni belole.
    Mutasd a teljes hozzászólást!
  • Kedves Erdeszt!

    Köszönöm szépen javításaidat, igazad van.
    Figyelmetlenségből nem olvastam el a feladatot, pontosabban szólva átugrott a fő kérdés fölött a szemem, és csak a próbálkozási kódot, illetve a tesztet olvastam el.

    Azt hittem, hogy a hugeHDD egy egyszerű limitszűrés, a tesztből úgy sejtettem, 1000 fölé szűr. A hozzászólásom így nem alkalmas a feladat megválaszálására, bár, egyetlen haszna az, hogy legalább a szintaxist tisztázza, épp azt, amiről Te is írtál első hozzászólásodban.

    Ami a feladatot illeti, a továbbiakban tanácsodat megfogadva én is lépésekre próbálom bontani, hogy ne rontsam el a tanár munkáját.

    Kedves Teki19!

    Ahogy látom, a feladat az alábbi részfeladatokból áll.

    1) részfeladat: A kapacitás-maximumot kiszámoljuk, de csak az SSD-kre vonatkozóan. (Hiba lenne a maximumot az összes tárolóra nézve számolni).

    Ezt az első részfeladatot megírhatnánk egyetlen fügvénnyel is, most első megközelítésben viszont mindent kinosan szétbontok, és még ezt az első részfeladatot magát is két képésben teszem meg.
    Két külön segédfüggvény lesz, kétszer  megyünk végig a listán, teljesen szétválasztjuk a fenti két szempontot. (Ez bírálható megközelítés, de egyelőre belefér, úgyis könnyű lesz utólag fölülemelekedni ezen és később optimalizálni, szépíteni)

    Tehát két segédfüggvényt fogalmazunk meg:

     1 a) az első segédfüggvény kiválogatja a tárolók összlistájából az SSD-típpusúakat, és összeállítja ezek méreteinek listáját. Maximumkereséssel ebben a lépésben nem foglakozunk.
    Tehát egyelőre egy

    selectSSDCapacityValues :: [Storage] -> [Int]

    segédfüggvényünk legyen. Ez könnyen megírható a már korább a kérdében szépen megírt isSSD függvény alapján. (Valójában Te isHDD függvényt írtál, egyszerűség kedvéért írj meg egy isSSD függvényt is, ezt itt még kényelmesebben használhatod).

    Tegyük fel tehát, hogy már meg is van a selectSSDCapacityValues függvény.

    Van tehát egy számlistánk (amit e függvényünkből kaphatunk), e számlistában tehát immár szigorúan csak az SSD-tárolók kapacitásai vannak, mondjuk [500, 250].

    A tesztben emltett első példán bemutatva:

    selectSSDCapacityValues [HDD "Seagate" 5600 250, HDD "Verbatim" 7200 1000, SSD "Samsung" 500, SSD "Samsung" 750]

    eredménye az legyen, hogy

    [500, 750]

    1 b)
    Mi lenne a következő lépés? Ezt az eredményt rögtön beletöltjük egy másik segédfüggvénybe,  amely viszont csak maximumkereséssel foglakozik. Tehát tárolótipusokkal, kapacitásokkal e függvénynek nem kell foglalkoznia: legyen egy csontmeztelen tisztán számokra szorítkozó tiszta matematikai maximumkereső függvényünk:

    calculateMaximum :: [Int] -> Int

    A részleteket most is kihagyom, azt megemlítem, hogy az üres lista esetét most ne komplikáljuk túl:

    calculateMaximum [] = error "Nincs miből maximumot válogatni"
    calculateMaximum [n] = n
    calculateMaximum (n : ns) = .....

    Az üres lista okozta hibalehetőség esetére majd visszatérünk a végén, egyelőre első körben az üres lista esetét nem kezeljük le, helyette az egyelemű listára adjuk meg a ,,végső eset'' kezelését.

    Visszatérve a tesztbeli példára:

    calculateMaximum [500, 750]

    eredménye legyen

    750

    Nyilván a két függvényt értelemszerűen össze fogjuk dugni. Megintcsak a teszten bemutatva:

    calculateMaximum (selectSSDCapacityValues [HDD "Seagate" 5600 250, HDD "Verbatim" 7200 1000, SSD "Samsung" 500, SSD "Samsung" 750])

    eredményétől azt várjuk el hogy legyen

    750.

    Úgy is mondhatnám, hogy a

    selectSSDCapacityValues :: [Storage] -> [Int]

    függvényből és a

    calculateMaximum :: [Int] -> Int

    függvényből összerakunk egy

    calculateMaxCapacityAmongSSDsOnly :: [Storage] -> Int
    calculateMaxCapacityAmongSSDsOnly = calculateMaximum . selectSSDCapacityValues


    függvényt, amely a tárolók összlistájából kiszámolja (szigorúan persze azon belül csak az SSD-ken belül nézve) azt a maximumot, azt a konkrét számot, amivel majd tovább tudunk haladni a feladat megoldásában!

    Az első részfeladat tehát megvan.

    Jöjjön a feladatot lezáró második részfeladat

    2)


    Térjünk vissza a tárolók eredeti (ömlesztett) összlistájához! Az a jó hír van, hogy a tárolók fajtájával már nem is kell majd foglakoznunk. Egyszerűen leválogatjuk az eredeti tárolóösszlistbáól a fenti érték (a teszt példája esetében 750) feletti kapacitású tárolókat: ez lesz a végső válasz a feladat kérdésére.

    Azért nem kell itt foglakoznunk a tárolók típusával, mert maguk az egyes SSD-tárolók kapacitásukban nyilván nem haladhatják meg az előzetsen épp a saját körükön belül kiszámolt maximumot, tehát az SSD-tárolók ,,automatikusan'' kihullanak. Így a tároló fajtája szűrésével nem is kell foglalkozni, elvileg elég az is, ha csak kiválogatjuk a korábban már megkapott maximumnál nagyobb kapacitású tárolót az összes tároló közül: ez a válogatás is helyes mogoldást adna.

    Tehát a feladat lezáró részfeladata egyszerűen az, hogy írjunk egy

    filterByCapacityAboveLimit limit :: Int -> [Storage] -> [Storage]
    filterByCapacityAboveLimit limit [] = []
    filterByCapacityAboveLimit limit (storage : storages) = ...

    ennek megírásához hasznás a rekurzióból természetes módon következő szűrési logikát! A tárolók fajtájával nem kell törődnöd, a kapacitás lekérdezéshez egyszerűen használd az Általad a kérdés kiírásánál jól megírt

    capacity :: Storage -> Int

    függvényt.


    Ha ez megvan, akkor a feldat minden részlépése megvan, most össze kell rakni a meglevő részfeladatokat a teljes feladattá. Itt egy kis konkrét szintaktikai trükk van, ezt bemutatom, mert tulajdonképp az eredeti kérdés is épp az ezzel kapcsoaltos szintaktikai hibákra kérdez rá:

    hugeHDDs :: [Storage] -> [Storage]

    hugeHDDs allStorages = let maxSDDCap = calculateMaxCapacityAmongSSDsOnly allStorages in filterByCapacityAboveLimit maxSDDCap allStorages

    van egy lehetséges alternatív szintaxis is ugyanennek a fajta összerakásnak a megoldására:

    hugeHDDs allStorages = filterByCapacityAboveLimit maxSDDCap allStorages where maxSDDCap = calculateMaxCapacityAmongSSDsOnly allStorages

    Megvagyunk.

    Egy érdekesség: ha a tárolók összlistája üres, akkor is lefut a program, pedig --- emlékezzünk rá --- a calculateMaximum segédfüggvény nem kezeli le az üres lista esetét. Ennek oka az, hogy üres lista esetében a hugeHDDs ,,főffüggvény'' le sem futtatja a calculateMaximum segédfüggvényt, ilyenkor a segédfüggvény vizsgálata nélkül üres eredményt ad. A Haskell ún. ,,lusta kiértékelése'' meg épp ezt ,,kezeli'' le jól.

    Egyébként nem kell a feladatot feltétlenül ennyire részlépesekre szedni. Lehet nagyobb lépésekben is dolgozni, illetve esetleg máskép tgolni a részlépéseket. Fontos viszont mindenképp, hogy a maximumot az SSD-kre nézve kell számolni, tehát ha ennek számolása egy lépésbe történik, akkor erről mindenképp gondoskdni kell.
    Mutasd a teljes hozzászólást!
  • calculateMaximum - Van ra beepitett fv ugy hivjak, hogy maximumBy

    Azért nem kell itt foglakoznunk a tárolók típusával, mert maguk az egyes SSD-tárolók kapacitásukban nyilván nem haladhatják meg az előzetsen épp a saját körükön belül kiszámolt maximumot, tehát az SSD-tárolók ,,automatikusan'' kihullanak.

    Ez jo meglatas, nem gondoltam ra

    ennek megírásához hasznás a rekurzióból természetes módon következő szűrési logikát!

    Miert nem csak a filter fv-t hasznalod?

    Egy érdekesség:...

    Mi van ha nem ures a lista de nincsenek benne ssd-k?

    Amugy nem nagyon latom ertelmet az isHDD es capacity seged fv-eken kivul mast definialni, csak szet tordeled vele az algoritmust es nehezebb lesz olvasni a kodot. Egyben sem olyan veszes:

    hugeHDDs :: [Storage] -> [Storage] hugeHDDs storages = let (hdds, ssds) = partition isHDD storages in if null ssds then hdds else let maxSsdCapacity = capacity (maximumBy (compare `on` capacity) ssds) in filter ((> maxSsdCapacity) . capacity) hdds
    Mutasd a teljes hozzászólást!
  • Kedves Erdeszt!

    Köszönöm szépen válaszodat!

    Köszönöm azt is hogy mgmutattad, hogy a HDD-ket tartalmazó, de SDD-kből egyet sem tartalmazó lista esetén a maximumkeresés parciális mivolta hibához vezet!

    Ez egyáltalán nem jutott eszembe. (A partition használata egy pillanatra igen.)

    Viszont a most alább csatolandó mintamegoldásomban a maximumBy függvény használata helyett egy egészen más irányú általánosítását használnám a maximumkeresésnek.

    Mindenképp totális függvényt szeretnék használni a maximumkeresére, és még feltételvizsgálattal korrektül lekezelve sem akarok most használni parciális függvényt. Csak kiváncsiságból nézzük meg e szemléletet.

    A legeszszerűbb -- kissé matematikai ízű -- megoldás, ha az üres halmaz (lista) maximumát minusz végtelennek definiéljuk. Tudjuk az algebrából, analízisből, hogy ez algebrailag korrekt és jól általánosuló, korrekt definíció.

    A csatolt listában a hugeHDDs függvény mutatja ennek a megközelítésnek egy „gyorsmegoldását”. Ahogy látszik, a minBound::Int érték képviseli a minusz végtelent. (A automatikus típuskövetkeztetés miatt elég minBound-ot írni.)

    A lényeg, hogy azezzel kapcsolatos esetszétválasztás nem töri szét a sorokat, mert a foldr függvény (amely a lista adatszerkezet „természetes” lebontó művelete, katamorfizmusa) épp jól magába tudja sűríteni ezt a fajta „átemelést”.  

    Egy, a feladat gyakorlatából jelentéktelen, de a matematikai szigor szempontjából bosszantó hiba azért van ezzel a megoldással. Mi van, ha a feladatbeli HDD-tárolók kapacitása épp megegyezik a  minBound::Int értékkel? Bizony akkor a teszt elbukik. Bár élő feladatban  a kapacitás csak nemnegatív szám lehet, így e hiba a feladat világában gyakorlatilag  nem jelentős, de a Haskell programozók ízlése által megszokott típusbiztonság szempontjából e hiba igenis bosszantó. Főleg amikor az Agdában még a rendezett lista invariánsa és a vektorok méretének indexelése is kaphat fordítási idejű típusbiztonságot -- idáig persze most nem kell elmennünk, itt egyszerűbb eszközök is elegendőek.

    Ezért a mellékelt megoldás egy idevonatkozó  típusbiztos megoldást próbál bemutatni, ezt képviseli a hugeHDDs' függvény, amelyre szintén külön is futtathatóak a tesztek (hugeHDDSTest').

    Az alternatív megoldás alapötlete, hogy a negatívvégtelen fogalmát algebrai adattípus szintjén vezetjük be, vagyis típusoperátorokkal bővítjük ki az Int alaptípust úgy, hogy az minden létező Int értéktől külön tartalmazza a minuszvégtelen fogalmát.

    Bár ezt lehetne egy

    data IntOrNegativeInfinity = Ordinary Int | NegativeInfinity

    külön algebrai adatpus bevezetésével is megoldani, amire külön rendezési segédfüggvényeket defniálnánk, de szerencsénkre felesleges itt egyéni definíciókhoz nyúlnunk, hiszen a Haskellben van erre beépített megoldás is, hogy egy típust egyetlen külön értékkel bővítsünk. Ez a Maybe.

    Az meg külön a szerencsénk, hogy a Haskellben a Maybe rendezése is definiálva van (Ord typeclass), és szerencsénkre épp úgy, hogy

    Nothing < Just _

    Ez épp a kezünkre jön! A Maybe Int-ben a Nothing természetes módon játssza a  minuszvégtelen szerepét. (Minumumkeresős feladatban, ahol a pluszvégtelennel kell babrálni, ott kissé bonyolultabb lenne, de hát itt most pont a jó irányú feladat áll előttünk!)

    A csatolt fájlban a hugeHDDs' függvény mutatja ezt a vonalú megoldást.
    Mutasd a teljes hozzászólást!
    Csatolt állomány

  • A legeszszerűbb -- kissé matematikai ízű -- megoldás, ha az üres halmaz (lista) maximumát minusz végtelennek definiéljuk

    Itt majdnem elsirtam magam egy kicsit de a masodik megoldasod(Maybe-s) tetszik
    Mutasd a teljes hozzászólást!
  • Eszembe jutott meg egy megoldas a partial maximumBy problemara:

    data Nel a = MkNel a [a] nel :: [a] -> Maybe (Nel a) nel [] = Nothing nel (x:xs) = Just (MkNel x xs) instance Foldable Nel where foldr f init (MkNel x xs) = foldr f (f x init) xs
    Majd a hugeHDDs-ben az if helyett irhatsz `case nel ssds of`
    Igy a maximumBy meg mindig partial de a kollekcio garantaltan nem ures.
    Mutasd a teljes hozzászólást!
  • A legeszszerűbb -- kissé matematikai ízű -- megoldás, ha az üres halmaz (lista) maximumát minusz végtelennek definiéljuk

    Itt majdnem elsirtam magam egy kicsit de a masodik megoldasod(Maybe-s) tetszik

    Pedig épp a minusz végtelens gondolat eredete a legszilárdabb, a topológiából és más analóg területekről vett tételek ihlették.

    És valójában a Maybe-s megoldás sem más , mint a minusz végtelen  type-safe modelezése, teljesen ekvivalens a mögöttes matematikai modellt tekintve (a Maybe Int-ben a Nothing jól modellezi a minusz végtelent). Hogy helyes eredményt ad, az könnyen látható, de ennél is fontosabb, hogy maga  az alapszemlélet sem ad hoc jellegű, hanem egy a matematika sok területén analóg módon előforduló definíciók állnak a hátterében.

    Már a topológiában, sőt már a hálóelméletben is megszokott, hogy az üres halmaz (vagy az annak megfelelő elem) szuprémuma szerepét olyan elem tölti be, ami a teljes univerzumra vonatkozóan éppen az infimum (és fordítva).

    sup {} = minusz végtelen
    inf {} = plusz végtelen

    sup R = plusz végtelen
    inf R = minusz végtelen

    Ezzel analóg az a halmazelméleti azonosság, hogy az üres halmazcsalád (mint indexelt halmaz) együttes uniójának az üres hamazt, együttes metszetének pedig a teljes univerzumot tekintjük (ebből az utóbbi az, ami első látásra kicsit meglepő):

    BigUnion {A_i | i valamilyen indexeléssel} = A1 union A2 union A3 ...

    speciális esetei a

    BigUnion {} = {}


    és a

    BigMetszet {A_i | i valamilyen indexeléssel} = A1 union A2 union A3 ...

    speciális esete pedig a

    BigMetszet {} = Univerzum

    Ugyanaz a fordítottnak tűnő logika: éppen a ,,csökkentő'', ,,elvevő'' jellegű nek gondolt művelet (a metszet) az, amely az üres esetben pont hogy a ,,legnagyobb'' globális elemet adja, és épp a ,,növelő'', ,,hozzátevő'' jellegű múvelet (az unió) 
    adja üres esetben a globálisan ,,minimális'' elemet.


    A mgöttes háttér igazából ugyanarra a sémára épül fel, minthogy a listára vonatkozó AND művelet az üres listára true-t ad, a listára vonatozó OR müvelet pedig üres listára false-ot. (noha épp az AND a ,,szűkmarkú'' művelet, az OR pedig a ,,bőkezű''). De a sima összeadás, és szorzás is ugyanezt a meglepetést nyujtja:

    and :: [Bool] -> Bool
    and = foldr (&&) true
    and [] ------------------------> true 

    or :: [Bool] -> Bool
    or = foldr (||) false
    or []  ------------------> false


    sum :: [Int] -> Int
    sum = foldr (+) 0
    sum [] ------------------------> 0

    product :: [Int] ->Int
    product = foldr (*) 1
    product [] ------------------> 1

    Majd szeretném megélni, ha a jövöben valamikor sikerül a topológiával, algebrával, akár vérmesebb reményeim szerint a kategoriaelmélettel megismerkednem, akkor könyebb lesz-e a Haskell könyvárak logikájának, később akár tervezésének a megértése.

    Régebben femerült bennem a kérdés, hogy vajon az UML szerepét mi tölti be a Haskellben. Valaki a Quorán vagy a Stackoverflowon erre azt válaszolta - talán félig viccből --, hogy ,,Hát a kommutatv diagrammok!''. Persze elhangzott a Coq, sőt általában a kategóriaelmélet neve is. Én ugyan többször is próbáltam ezeknek nekimenni, de végül e terveim rendre félbemaradtak. Most viszont lassanként ugy tűnik, hogy a Martin-Löf tipuselmélet és az Agda egy kicsit kezd megfogni engem, de ez is még nagyon az eleje csak. Egyelőre hagyom vitetni magam velük, aztán majd talán mégegyszer nekimengyek a kategoriaelméletnek és a topológiának egy kicsit később. Azt sejtem, hogy ebben van a lényeg, a haskell ezeknek csak a lenyomata, árnya.
    Mutasd a teljes hozzászólást!
  • instance Foldable Nel where
        foldr f init (MkNel x xs) = foldr f (f x init) xs

    Köszönöm szépen ezt a megoldást is.
    A fold-okat egészében is régóta meg szerettem  volna fogom tekinteni részletesebben. Végső eredetüket tekintve a foldr az nem más mint valami kategoriaelméleti fogalom, a katamorfizmus egyws konkrét megnylvánulásai. Ez régi adósságom, hogy ezt jobban megismerjem valamikor.
    Mutasd a teljes hozzászólást!
  • Koszi, erdekes olvasmany volt. Matematikai szempontbol igazad van de ez a megoldas eleg C szerunek tunik(specialis jelentessel felruhazni az ertekkeszlet egyik(vagy tobb) elemet).

    Persze elhangzott a Coq, sőt általában a kategóriaelmélet neve is. Én ugyan többször is próbáltam ezeknek nekimenni, de végül e terveim rendre félbemaradtak.

    Probaltad a Software Foundations sorozatot? Ugyan csak az elso konyv felet olvastam de nekem nagyon bejott es sokat segitett megerteni a dependent tipusokat es a kapcsolatukat a logikaval(Coq-ot hasznal bar azt hiszem van valami hasonlo Philip Wadler-tol ami Agda-t hasznal).
    Mutasd a teljes hozzászólást!
  • Kedves Erdeszt!

    Köszönöm szépen válaszodat!

    Igen, az elmúlt hó előtti hónapot a Software Foundations sorozat első könyvével töltöttem. Szerencsére a korábbi próbálkozásaimtól eltérően (tavaly, meg öt éve), most sikerült ,,vonóerőt nyerni'' a dologban.

    Talán a tavaly félig elolvasott Type theory and functional programming ingyenes PDF-könyv ágyazott meg neki (Simon Thompson). Itt sokat segítettek a csak papírt és ceruzát igénylő logikai levezetési fák a szimpla természetes levezetés begyakoroltatásával, és a sok apró gyakolat (pl. a De Morgan összefüggések levezetetése szigorúan a természetes levezetés eszközkészletein belül). Aprómunka, de végül ez tudott megágyazni a Martin-Löf típuselméletnek, ami azelőtt évekig frusztrálóan megugrhatatlan volt számomra.

    Vicces, hogy kiderült, hogy a két De Morgan szabály két-két irányából, tehát az összesen 4 összefüggésből egész pontosan három vihető át az intuicionista logikába (az egyik De Morgan tétel az egyik irányban ott nem igaz).

    Köszönöm szépen, hogy írtál Philip Wadler: Programming langues foundations in Agda művéről. A Software Foundations-nak az Agda irányű megfelelőjét bemutató műre épp vágyam is volt, köszönöm szépen hogy megmutattad.

    Van egy kis mátrixszámítási könyvtáracskám: ütközésvizsgálat. Kb. a Gauss-kiküszöböléshez hasonló algoritmussal dolgozik (egész pontosan a Fourier-Motzkin eliminációval), és konvex sokszögekre végez afféle ,,collision detectiont'' (amit ki lehet terjeszteni konkáv poligonokra is). Haskellben és JavaScriptben írtam még tavalyelőtt, egy ingatlancégnek szóló alaprajztervező editor projektem részeként, de most a hetekben ezt át fogom írni Agdába. Ennek két oka van:

    1) a függő típusok miatt épp mátrixokra és vektorokra (adott hosszra rögzített, dimenzió függő típus) ngyon szép öndokumentáló programot lehet írni Agdában (vagy Coq-ban).

    _×_ : ∀ (Típ : Set) (k m n: ℕ) → Mátrix Típ k m → Mátrix Típ m n → Mátrix Típ k n
    ....

    transpose : ∀ (Típ : Set) (m n: ℕ) → Mátrix Típ m n → Mátrix Típ n m
    transpose = ...


    proof-transpose-idempontence : ∀ (Típ : Set) (m n  : ℕ) (mátrix :  Mátrix Típ m n) → transpose (transpose mátrix) ≡ mátrix
    proof-transpose-idempontence = .....


    2) Szép természetes módon lehet a téma során természetes módon adódó tételeket, és bizonyításukat  is szerepeltetni a program részeként (pl. hogy mátrix transzponáltjának transzponáltja önmaga).

    Így sokkal jobban karban lehet tartani majd a program dokumetációját, egyúttal afféle etalonpéldányként magát a forrást is. ez így azthiszem tömörebb és kifjeezőbb lesz, mint bármi más volna.

    Ilyet semmi más nyelvben nem tudnék ilyen tömörséggel összefogni (a LaTeX-et leszámítva, de úgy értem, azonnal típusellenőrizhető programnelvként is egyúttal)-
    Mutasd a teljes hozzászólást!
abcd