Fórum Root.cz

Hlavní témata => Vývoj => Téma založeno: Coati 26. 02. 2022, 11:27:14

Název: Číselné typové parametry a type erasure
Přispěvatel: Coati 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?
Název: Re:Číselné typové parametry a type erasure
Přispěvatel: Filip Jirsák 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.
Název: Re:Číselné typové parametry a type erasure
Přispěvatel: Idris 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.
Název: Re:Číselné typové parametry a type erasure
Přispěvatel: Idris 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
Název: Re:Číselné typové parametry a type erasure
Přispěvatel: Filip Jirsák 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ě.
Název: Re:Číselné typové parametry a type erasure
Přispěvatel: Idris 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í.
Název: Re:Číselné typové parametry a type erasure
Přispěvatel: Idris 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.
Název: Re:Číselné typové parametry a type erasure
Přispěvatel: Idris 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