Compiler Seminar

[Daniel Berenyi]

Sziasztok!

Akkor mivel nem volt nagyon nagy ellenkezdés, javaslom, hogy a következő meetinget most Szerdán, délután 5 órától tartsuk.

Link:

https://meet.google.com/nox-sqmf-auz

Lehel Gábor beszélne a subtyping ötleteiről, bemásolom a korábbi leveléből az alábbi részletet:

Nemrég találtam egy módját a subtyping meg a unificationös type inference összeegyeztetésének ami kevesebbet tud, mint az algebraic subtyping / mlsub, cserébe egyszerűbb; vagy másik oldalról valamivel többet tud / jobban működik mint a 'naiv' unification és nem sokkal bonyolultabb. (Még nem teljesen 100%, hogy ez valóban működik, de néhány kör oda-vissza után már ott tartok, hogy úgy mondjuk 90%; ha befejezem a kis prototípust amit elkezdtem akkor remélhetőleg pozitív irányba változik majd ez a szám.)  És szívesen mésélnék arról hogy egyrészt ezek a szavak mit jelentenek :), egyáltalán mi volt az eredeti probléma amire ez született megoldásként, meg esetleg az 'algebraic subtyping'ot is felvázolni és ahhoz viszonyítani, ill. András említette múlt héten, hogy ő is implementált egy coercive subtyping-ot, aminél a metaváltozók kezelésénél vannak a komplikációk, és szívesen összevetném azzal is, ha neki is vannak erre jó ötletei (mint általában szoktak lenni).

üdv,

Dani

[Daniel Berenyi]

Emlékeztető.

D.

[Whisperity]

Sziasztok!

Lehet hogy ezt nekem ma sajnos skippelnem kell, mert ha 7kor indulok
el haza cégtől, akkor a kijárási tilalom előtt nem érkezem már haza.
Az lehet még, hogy út közben bedobom a fülest és behívok. Bár úgyse
szoktunk semmi titkosról beszélni.

> --
> 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/CABmfui0jyBaY0Rv8f-5-HqP%3Du1b6rZweBkUT3n%3DGhvzw6570%3Dw%40mail.gmail.com.

[Daniel Berenyi]

Sziasztok!

Ma Gábor beszélt a subtyping - type checker eljárásokról, aminek a pszeudokódos linkje magyarázatokkal itt van:

https://gist.github.com/glaebhoerl/f68c6805fd00dff6240500e49298f9c1

Illetve itt a cikk az mlsub eljárásról, ami elvileg érthető:
https://lptk.github.io/programming/2020/03/26/demystifying-mlsub.html

üdv,

D.

[Gábor Lehel]

Illetve itt a cikk az mlsub eljárásról, ami elvileg érthető:

...az eredetihez viszonyítva, legalábbis :P

Közben előkerestem egy másik kapcsolódó posztot is:

http://smallcultfollowing.com/babysteps/blog/2014/07/09/an-experimental-new-type-inference-scheme-for-rust/

Mikor ezt még 2014ben olvastam, semennyire sem vágtam a type inference-et, és így nem is értettem sokat belőle.

Akkortájt amikor az eredeti algebraic subtyping cikk+disszertáció megjelent, és említve volt benne ez a "structural subtyping" megszorítás (amikor különböző típuskonstruktorok nem lehetnek altípusozási relációban, és csak a paraméterek közötti viszony a meghatározó), visszakerestem, mert észrevettem, hogy ez a megszorítás igaz a Rust-ra: "csak a lifetimeokra" van subtyping a Rustban. És felderengett hogy volt régen egy poszt vmi furcsa új type inference eljárásukról, lehet-e vajon köze.... és a leírt algoritmus számomra valóban úgy tűnik, hogy kihasználja a tulajdonságot. (És emiatt is kerestem most elő megint.)

És most hogy újból olvasom, látom, hogy használ postponing-ot is (amiről azóta már azt is tudom, hogy így neveznek), meg szerepel benne a típus-alapú rezolúció problémája is. Meg most már kíváncsi vagyok arra is, hogy milyen lehetett vajon a korábbi algoritmusuk, amiről erre tértek át... állítólag valami Hindley-Milneres, ugyanakkor meg "we track a lower- and upper-bound over time", szóval nem is csak.

Lábjegyzetek:

 * Nem tudom, hogy ma is ezt használják-e még, de nincs is ezzel ellenkező értesülésem.

 * Amit az előadásban említettem "glitcheket" azok a Rustban nem a lifetimeoknál jönnek elő, hanem az egyéb automatikus konverzióknál, mint az &mut T-ről az &T-re való. (Ők ez utóbbiakat nem hívják "subtypingnak", mert típuskonstruktorok alatt nem működik (nincs rá variance), hanem csak 'elsőrendű' esetekben; helyette a "coercion" szót használják, ami megint más, mint amit a Haskellesek értenek azalatt, és nem tudom hányféle jelentése lehet még. De mindenesetre ők ezekre használják a tárgyalt bidirectional checking + subtypingos módszert.)

 * A posztban említi, hogy "If we wanted to extend the scheme to handle more kinds of inference beyond lifetimes, it can be done by adding new kinds of inference variables. For example, if we wanted to support subtyping between structs, we might add struct variables", amiben én most kételkedek, mivel ez már nem férne bele abba a megszorításba. De aztán könnyen lehet, hogy ő tudja jobban.

Ha szeretné megtekinteni ezt a beszélgetést az interneten, látogasson el ide: https://groups.google.com/d/msgid/compiler-seminar-budapest/CABmfui3ESTx-4Z8GJsC8F3Q1RV-A8fW3o%3DSXH06Y3SZG_d4M0g%40mail.gmail.com.