marc 17-i eloadas: gepikod szemantika modellezes (compilerhez) Idris-2-ben
8 views
Skip to first unread message
Csaba Hruska
Mar 10, 2021, 5:09:43 AM3/10/21
to compiler-seminar-budapest
Sziasztok,
Szereztem eloadot a kov heti szeminariumra (marc 17. 17:00).
Divianszky Peti adja majd elo a projektjet amit Idris2-ben ir es gyakorlatilag egy assembler ami egy minimalista gepikodu nyelvet modellez maximalisan magas szemantikaval. A magasabb szintu resze a compiling to categories megkozelitest koveti. (http://conal.net/papers/compiling-to-categories/)
Ha jol ertem a projekt celkituzese a nagyon alacson szintu programozas leirasa nagyon magas (tipus) szintu modellezese, ami jol jon helyes es hatekony kodgeneralashoz.
Csaba
ÉRDI Gergő
Mar 10, 2021, 5:18:30 AM3/10/21
to Csaba Hruska, compiler-seminar-budapest
On Wed, 10 Mar 2021, Csaba Hruska wrote:
> Szereztem eloadot a kov heti szeminariumra (marc 17. 17:00).
Fel vannak veve ezek a szeminariumok? Van valahol egy szaftos Youtube
> Szereztem eloadot a kov heti szeminariumra (marc 17. 17:00).
csatorna?
Csaba Hruska
Mar 10, 2021, 5:32:10 AM3/10/21
to ÉRDI Gergő, compiler-seminar-budapest
nincs
ÉRDI Gergő
Mar 10, 2021, 5:38:05 AM3/10/21
to Csaba Hruska, compiler-seminar-budapest
On Wed, 10 Mar 2021, Csaba Hruska wrote:
> nincs
Es medve, nem akarsz lehuzni a halal-listadrol?
Akarom mondani, nem lehetne hogy legyen?
Daniel Berenyi
Mar 17, 2021, 6:32:22 AM3/17/21
to Csaba Hruska, compiler-seminar-budapest
Sziasztok!
Akkor ez lesz ma (l. Csaba levelét alább) 17:00-tól.
üdv,
Dani
--
Azért kapta ezt az üzenetet, mert feliratkozott a Google Csoportok „compiler-seminar-budapest” csoportjára.
Az erről a csoportról és az ahhoz kapcsolódó e-mailekről való leiratkozáshoz küldjön egy e-amailt a(z) compiler-seminar-b...@googlegroups.com címre.
Ha szeretné megtekinteni ezt a beszélgetést az interneten, látogasson el ide: https://groups.google.com/d/msgid/compiler-seminar-budapest/CANjChEruqhdNmKLjVZGS5YsXtjn4vrN0pDQzfBDJeTxnDG--Jw%40mail.gmail.com.
Daniel Berenyi
Mar 17, 2021, 2:31:06 PM3/17/21
to Csaba Hruska, compiler-seminar-budapest
Sziasztok!
Ezek (l. alább) voltak a mai beszélgetésben, most nem volt erőm végig filterezni.
Csaba majd ír a felvétellel kapcsolatban, illetve ha el lehet kérni a prezentációs pdf-et Pétertől az jó lenne.
üdv,
D.
-------------------------
Andor Pénzes
http://conal.net/papers/compiling-to-categories/
Interaction nets: https://en.wikipedia.org/wiki/Interaction_nets#:~:text=Interaction%20nets%20are%20a%20graphical,proof%20structures%20of%20linear%20logic.&text=Interaction%20nets%20are%20at%20the,%2C%20in%20L%C3%A9vy's%20sense%2C%20Lambdascope.
Gergő Érdi
https://www.reddit.com/user/SrPeixinho/submitted/ ez a faszi szokott /r/haskell-re optimalis lambda calculus redukciorol posztolni
---------
Balazs Komuves
17:51
de ez eddig teljesen az arrows (esetleg casual commutative arrows?)
csak a Haskell arrow asszimetrikusan van megfogalmazva (product -biased), de ez csak tortenelmi felreertes
Gergő Érdi
17:52
Balazs: `arr` nelkul, krucialisan
Balazs Komuves
17:52
igen de az hibas belevenni
defaultbol
az is tortenelmi felreertes :)
Gábor Horváth
18:01
bocsi nekem mennem kell, de majd varom a felvetelt :)
Gergő Érdi
18:01
LESZ FELVETEL?!?!?!
Ön
18:01
elvileg Csaba csinálja
Balazs Komuves
18:01
csaba valamit elinditott a sajat gepen
Gergő Érdi
18:02
tok jo mert direkt kerdeztem tole h fel lesz-e veve, akkor nem biztos h ejjel kettoig itt maradnek :)
Andor Pénzes
18:02
Mennyi az idozonas elteres?
Gergő Érdi
18:02
most me'g csak 1 ora van
2 a vegere lesz
Balazs Komuves
18:03
utc+8 ?
Gergő Érdi
18:03
aha
András Kovács
18:04
binding time analysis
Gergő Érdi
18:10
minden nemlinearis valtozo-hasznalatbol dup lesz, nem?
Balazs Komuves
18:10
de
Gergő Érdi
18:20
pont ezt akartam kerdezni :)
Balazs Komuves
18:20
igen, az ADT-ket hogyan fogod csinalni
ez volt a kerdes
Andor Pénzes
18:21
Sum of products?
Generics?
Balazs Komuves
18:31
erdemes lenne megnezni nem csak permutaciokat
Gergő Érdi
18:31
vegulis minden lambda term csak permutacio, csak nehany valtozo felett van egy fuggvenyalkalmazas
Balazs Komuves
18:31
el tudom kepzelni hogy a permutacio egyszerubb, mert sosincs dup / elvesztes
a permutacio invertalhato :)
a legtobb program nem
Gergő Érdi
18:32
de eddig amikor Peti "permutaciot" mondott akkor mindig azt ertette alatta h ismetleses-kihagyasos
Balazs Komuves
18:33
de a kodban permute fuggveny volt
kerdes az mit csinal :)
Gergő Érdi
18:33
oh
Gergő Érdi
18:42
l6 miben mas mint mondnuk a sub meg az add kozul "eltunt" label?
Balazs Komuves
18:43
cmp utan volt egy jump l6, az egy masik blokk. gondolom megmaradt a blokk hatar
Gergő Érdi
18:43
de azt hittem h mindig minden fel van annotalva ki meg be IP-kkel
szoval a sima sub is egy uj IP-re ugrik amikor vegez
Balazs Komuves
18:44
igen, es abbol inferal blokkokat
gondolom :)
Gergő Érdi
18:44
csak azokat ahogy Peti mondta "osszelinkeli"
de az l6 pont ugyanugy van a cmp utanra linkelve, elvileg
Balazs Komuves
18:45
igen
de filozofiailag, a cmp mindig egy blokk vege. gondolom ezt megtartotta (bar nem lenne muszaj)
Andor Pénzes
18:47
kolmogorov-complexity of the domain?
Gergő Érdi
18:49
de a kozeperol ki is ugorhatsz feltetelesen
es akkor paratlanra is mukodik
Balazs Komuves
18:49
unrollolod a loop belsejet
2x
akkor paros n-re nem kell talan xchg
de lehet hogy rosszul gondolom, jobban atgondolva :)
le kene irni
András Kovács
18:52
mi van, ha Idris-ben file-ból akarsz fordítani
akkor nem kapsz ingyen type inference-t
Gergő Érdi
18:55
szoval a kezi type inference-bol kijon egy egisztencialisan tipusozott lambda term, de utana mar minden tovabbi lepe tudod h tipustarto
András Kovács
19:08
CCC normalizáció Agda-ban: https://gist.github.com/AndrasKovacs/0da6864af7a8e386e671b66dc578ce39
Csak függvény + unit + product (azaz plain free CCC)
Gergő Érdi
19:24
koszi ez tok erdekes volt
Gergő Érdi
19:25
a Conal-cikkel en nem nagyon voltam megelegedve tbh
ahogy irtam az eloadas elejen is, sok reszlet nincs benne kifejtve
pl nyilt kifejezesek forditasarol
Balazs Komuves
19:27
a google-re fogjuk ra
hogy nem maradt ido :)
http://conal.net/papers/compiling-to-categories/
Interaction nets: https://en.wikipedia.org/wiki/Interaction_nets#:~:text=Interaction%20nets%20are%20a%20graphical,proof%20structures%20of%20linear%20logic.&text=Interaction%20nets%20are%20at%20the,%2C%20in%20L%C3%A9vy's%20sense%2C%20Lambdascope.
Gergő Érdi
https://www.reddit.com/user/SrPeixinho/submitted/ ez a faszi szokott /r/haskell-re optimalis lambda calculus redukciorol posztolni
---------
Balazs Komuves
17:51
de ez eddig teljesen az arrows (esetleg casual commutative arrows?)
csak a Haskell arrow asszimetrikusan van megfogalmazva (product -biased), de ez csak tortenelmi felreertes
Gergő Érdi
17:52
Balazs: `arr` nelkul, krucialisan
Balazs Komuves
17:52
igen de az hibas belevenni
defaultbol
az is tortenelmi felreertes :)
Gábor Horváth
18:01
bocsi nekem mennem kell, de majd varom a felvetelt :)
Gergő Érdi
18:01
LESZ FELVETEL?!?!?!
Ön
18:01
elvileg Csaba csinálja
Balazs Komuves
18:01
csaba valamit elinditott a sajat gepen
Gergő Érdi
18:02
tok jo mert direkt kerdeztem tole h fel lesz-e veve, akkor nem biztos h ejjel kettoig itt maradnek :)
Andor Pénzes
18:02
Mennyi az idozonas elteres?
Gergő Érdi
18:02
most me'g csak 1 ora van
2 a vegere lesz
Balazs Komuves
18:03
utc+8 ?
Gergő Érdi
18:03
aha
András Kovács
18:04
binding time analysis
Gergő Érdi
18:10
minden nemlinearis valtozo-hasznalatbol dup lesz, nem?
Balazs Komuves
18:10
de
Gergő Érdi
18:20
pont ezt akartam kerdezni :)
Balazs Komuves
18:20
igen, az ADT-ket hogyan fogod csinalni
ez volt a kerdes
Andor Pénzes
18:21
Sum of products?
Generics?
Balazs Komuves
18:31
erdemes lenne megnezni nem csak permutaciokat
Gergő Érdi
18:31
vegulis minden lambda term csak permutacio, csak nehany valtozo felett van egy fuggvenyalkalmazas
Balazs Komuves
18:31
el tudom kepzelni hogy a permutacio egyszerubb, mert sosincs dup / elvesztes
a permutacio invertalhato :)
a legtobb program nem
Gergő Érdi
18:32
de eddig amikor Peti "permutaciot" mondott akkor mindig azt ertette alatta h ismetleses-kihagyasos
Balazs Komuves
18:33
de a kodban permute fuggveny volt
kerdes az mit csinal :)
Gergő Érdi
18:33
oh
Gergő Érdi
18:42
l6 miben mas mint mondnuk a sub meg az add kozul "eltunt" label?
Balazs Komuves
18:43
cmp utan volt egy jump l6, az egy masik blokk. gondolom megmaradt a blokk hatar
Gergő Érdi
18:43
de azt hittem h mindig minden fel van annotalva ki meg be IP-kkel
szoval a sima sub is egy uj IP-re ugrik amikor vegez
Balazs Komuves
18:44
igen, es abbol inferal blokkokat
gondolom :)
Gergő Érdi
18:44
csak azokat ahogy Peti mondta "osszelinkeli"
de az l6 pont ugyanugy van a cmp utanra linkelve, elvileg
Balazs Komuves
18:45
igen
de filozofiailag, a cmp mindig egy blokk vege. gondolom ezt megtartotta (bar nem lenne muszaj)
Andor Pénzes
18:47
kolmogorov-complexity of the domain?
Gergő Érdi
18:49
de a kozeperol ki is ugorhatsz feltetelesen
es akkor paratlanra is mukodik
Balazs Komuves
18:49
unrollolod a loop belsejet
2x
akkor paros n-re nem kell talan xchg
de lehet hogy rosszul gondolom, jobban atgondolva :)
le kene irni
András Kovács
18:52
mi van, ha Idris-ben file-ból akarsz fordítani
akkor nem kapsz ingyen type inference-t
Gergő Érdi
18:55
szoval a kezi type inference-bol kijon egy egisztencialisan tipusozott lambda term, de utana mar minden tovabbi lepe tudod h tipustarto
András Kovács
19:08
CCC normalizáció Agda-ban: https://gist.github.com/AndrasKovacs/0da6864af7a8e386e671b66dc578ce39
Csak függvény + unit + product (azaz plain free CCC)
Gergő Érdi
19:24
koszi ez tok erdekes volt
Gergő Érdi
19:25
a Conal-cikkel en nem nagyon voltam megelegedve tbh
ahogy irtam az eloadas elejen is, sok reszlet nincs benne kifejtve
pl nyilt kifejezesek forditasarol
Balazs Komuves
19:27
a google-re fogjuk ra
hogy nem maradt ido :)
Kéri Kálmán
Mar 17, 2021, 3:16:29 PM3/17/21
to Daniel Berenyi, Csaba Hruska, compiler-seminar-budapest
Amikor Péter arról beszélt, hogy pl. összeadásnál megjegyzi a változatlanul maradt regisztert is, tudtam, hogy ez emlékeztet valamire, és most megtaláltam. (A táblázatot érdemes kinagyítani)
Ha szeretné megtekinteni ezt a beszélgetést az interneten, látogasson el ide: https://groups.google.com/d/msgid/compiler-seminar-budapest/CABmfui0ZyVHwBhaX-ufeXoiGEHQepvXuCuKm4MWY04V7k-NDJA%40mail.gmail.com.
Péter Diviánszky
Mar 17, 2021, 6:13:28 PM3/17/21
to compiler-seminar-budapest
Köszönöm a visszajelzéseket.
András CCC normalizációja tűnik a legrelevánsabbnak, de nekem változók nélkül és más konstrukciókkal lenne rá szükségem.
A reverse computation érdekes, de azt hiszem nem releváns.
Az \(a, b) -> (a + b, b) függvény invertálható, de ez a tulajdonságát nem használom ki.
n*log(n) < size(cat(t)) < n*log(n)*log(log(n))
ahol n = size(t).
Mivel megtaláltam a levelezőlistát, itt fogom jelezni később, hogy hogy haladtam a fordítóval.
Üdv:
Peti
András CCC normalizációja tűnik a legrelevánsabbnak, de nekem változók nélkül és más konstrukciókkal lenne rá szükségem.
A reverse computation érdekes, de azt hiszem nem releváns.
Az \(a, b) -> (a + b, b) függvény invertálható, de ez a tulajdonságát nem használom ki.
Megnéztem a cat: lambda->CCC komplexitását egy olyan benchmarkra is, ahol duplikációt és törlést is megengedek a változók között.
Tehát
t = \(x1,x2,...,xn) -> (y1,y2,...,yn),
ahol az y-ok bármelyike bármelyik x lehet.
Továbbra is t = \(x1,x2,...,xn) -> (y1,y2,...,yn),
ahol az y-ok bármelyike bármelyik x lehet.
n*log(n) < size(cat(t)) < n*log(n)*log(log(n))
ahol n = size(t).
Mivel megtaláltam a levelezőlistát, itt fogom jelezni később, hogy hogy haladtam a fordítóval.
Üdv:
Peti
András Kovács
Mar 18, 2021, 4:12:56 AM3/18/21
to Péter Diviánszky, compiler-seminar-budapest
A "változók" csak normálformákban vannak, eltűnnek triviális visszafordítással morfizmusokba.
Ha szeretné megtekinteni ezt a beszélgetést az interneten, látogasson el ide: https://groups.google.com/d/msgid/compiler-seminar-budapest/7b11bbe7-d5d8-428a-bf8d-ab5df46ab047n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages