Číselné typové parametry a type erasure

Coati

Číselné typové parametry a type erasure
« kdy: 26. 02. 2022, 11:27:14 »
Jak se v runtimu přistupuje k číselným generickým parametrům třeba u Vect<T,N>, když překladač provádí kompletní type erasure? Když jde o konstantu, dosadí ji překladač přímo, ale v některých jazycích N nemusí být známé při překladu, co tam je za trik?


Re:Číselné typové parametry a type erasure
« Odpověď #1 kdy: 26. 02. 2022, 12:40:23 »
Záleží na tom, o jakém jazyku píšete. Když se ptáte takhle obecně, dá se na to odpovědět akorát tak, že se k nim přistupuje úplně stejně, jako k jiným generickým parametrům.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Číselné typové parametry a type erasure
« Odpověď #2 kdy: 26. 02. 2022, 12:55:10 »
úplně stejně, jako k jiným generickým parametrům
K těm to v případě type erasure za běhu nejde vůbec.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Číselné typové parametry a type erasure
« Odpověď #3 kdy: 26. 02. 2022, 13:13:23 »
Kód: [Vybrat]
data Vect : Type -> Nat -> Type where
  Nil : Vect _ 0
  Cons : a -> Vect a n -> Vect a (n+1)
length : Vect a n -> Nat
length {n} _ = n
Instanci vektoru lze načíst například za běhu ze vstupu pomocí readVect.
Lze vyzkoušet zde: https://learn-idris.net/play

Re:Číselné typové parametry a type erasure
« Odpověď #4 kdy: 26. 02. 2022, 13:43:04 »
úplně stejně, jako k jiným generickým parametrům
K těm to v případě type erasure za běhu nejde vůbec.
No právě.


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Číselné typové parametry a type erasure
« Odpověď #5 kdy: 26. 02. 2022, 15:12:23 »
úplně stejně, jako k jiným generickým parametrům
K těm to v případě type erasure za běhu nejde vůbec.
No právě.
Ten kód výše ukazuje, jak se to řeší v případě type erasure. V backendu pro C nebo JS je krásně vidět, jak všechny typy zmizí.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Číselné typové parametry a type erasure
« Odpověď #6 kdy: 26. 02. 2022, 22:17:06 »
Kód: [Vybrat]
data Vect : Type -> Nat -> Type where
  Nil : Vect _ 0
  Cons : a -> Vect a n -> Vect a (n+1)
length : Vect a n -> Nat
length {n} _ = n
Instanci vektoru lze načíst například za běhu ze vstupu pomocí readVect.
Lze vyzkoušet zde: https://learn-idris.net/play
Ve v2 ten kód nefunguje, potřebná úprava je:
Kód: [Vybrat]
length : {n : Nat} -> Vect a n -> Nat
length _ = n
Tady je vidět ještě lépe, jak fungují tzv. implicitní argumenty.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Číselné typové parametry a type erasure
« Odpověď #7 kdy: 06. 03. 2022, 19:59:26 »
Tady je podrobně popsáno, jak se řeší $SUBJ v jazycích s lineárním typovým systémem: https://arxiv.org/pdf/2104.00480.pdf