Naivní závislostní typ (úvaha)

[BoneFlute]

Mějme hypotetický jazyk s hypotetickým typovým systémem.

Mějme typ Numeric reprezentující všechna reální čísla, a pak následující kaskádu typů:

Numeric > Int > Age > Young
Numeric > PositiveUnzeroNumeric
Kde Age je rozsah 0 - 255, Young 0 - 19, PositiveUnzeroNumeric rozsah 1 - MAX_INT

Máme funkci pro dělení:

Kód: [Vybrat]

div a b = a / b
A dáme jí takovouto typovou signaturu:

Kód: [Vybrat]

div :: Numeric -> PositiveUnzeroNumeric -> Numeric
Šlo by to? Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou? Možná ne, ale zajímalo, jestli by se k tomu někdo zkušenější mohl vyjádřit. Protože třeba:

Kód: [Vybrat]

calculate :: Numeric -> Numeric -> Numeric
calculate a b = a `div` (b - 3)
calculate 9 6 -- 3
calculate 9 3 -- divide zero
se IMHO nepřeloží.

Jaké to může mít úskalí?

[Reklama]

[gill]

Jaké to může mít úskalí?

funguje to jen s konstantními výrazy.

[BoneFlute]

Jaké to může mít úskalí?

funguje to jen s konstantními výrazy.

Můžeš to prosím rozvést? Co myslíš konstantními výrazy a co myslíš tím nefunguje.

[gill]

Jaké to může mít úskalí?

funguje to jen s konstantními výrazy.

Můžeš to prosím rozvést? Co myslíš konstantními výrazy a co myslíš tím nefunguje.

nebudu se dohadovat o definici konstantního výrazu. Tak jak jsi ten problém popsal, je snad jasné, že

Kód: [Vybrat]

calculate a b

kde a b jsou čísla z venku, žádnou compile time chybu generovat nemůže.

[BoneFlute]

Tak jak jsi ten problém popsal, je snad jasné, že

Kód: [Vybrat]

calculate a b

kde a b jsou čísla z venku, žádnou compile time chybu generovat nemůže.

Pokud myslíš něco jako:

Kód: [Vybrat]

main :: IO ()
main = do
    a <- getLine
    b <- getLine
    putStrLn $ format $ calculate (parseNumeric a) (parseNumeric b)
Tak mi je jasné, že fungovat bude. Respektive se to nepřeloží. V tomto by být problém neměl.

[Reklama]

[Jiří Havel]

Nějakou dobu jsem s něčím podobným experimentoval. Konkrétně otagované a ohraničené integery v C++. Je trochu problém vybalancovat poměr přínos/opruz.

1) Interakce s vnějším světem se děje furt. Balení a vybalování toho intu musí být jednoduché. Tvoje typy se vyskytují jen na pár místech. Postupně se rozlézají, ale i tak je interakce s vnějším světem jedna z nejčastějších věcí.
2) Nenulové číslo nevznikne jen tak, ale obvykle nějakým testem na nulu. Takže to balení není jenom na hranici tvého světa.
3) U intů je to jednoznačné, ale s floaty přicházejí další problémy. Takové typy jako "normalizovaný vektor" nebo "ortonormální matice" jsou v praxi dost fuzzy.

[Mirek Prýmek]

Na to ti bude umět dobře odpovědět Idris. Já jsem tu jím doporučenou knížku o dependent types ještě pořád nepřelouskal, takže pořádně ti odpovědět neumím, ale aspoň jeden problém tam vidím i tak:

Aby se to dalo nějak rozumně používat, musíš zároveň s tím zavést subtyping. Aby typový systém věděl, že Age je podmnožina Int. No a se subtypingem vzniká spousta otravných problémů, které asi nejsou neřešitelné, ale začnou typový systém a hlavně jeho syntaxi znepřehledňovat. V tématu o OOP jsem zmínil problém (ko|kontra)variance - můžeš do l: List Int vložit x : Age? Když ho potom z listu vybíráš, vrátí se ti Int nebo Age?

Haskell detailně neznám, ale myslím, že se subtyping do něj moc nehodí. Viz např. https://www.reddit.com/r/haskell/comments/423o0c/why_no_subtypingsubtype_polymorphism/

...no a druhá možnost je, že to nebudou podtypy. Pak to ale bude strašná otrava používat.

[Mirek Prýmek]

P.S. a jestli můžu už vyloženě vařit z vody, tak předpokládám, že když do typů zavedeš dostatečně silné formule, tak ti tam vznikne nějaký silný jazyk, což bude mít předpokládám dopady do rozhodnutelnosti a tak. Známe to, stačí někam prsknout Peanovu aritmetiku a je průser

(Idris mě omluví za humpoláckou mluvu a doupřesní to nebo opraví )

[Jiří Havel]

...no a druhá možnost je, že to nebudou podtypy. Pak to ale bude strašná otrava používat.

Další možnost je zneškodnit reference na mutable. Pokud subtyping funguje jen s referencema na const, případně s kopírováním/slicingem, tak je to relativně ok.

Samozřejmě že zůstává problém, že inkrement Age už není Age. Takže není možné napsat ani klasický for cyklus tak, aby to prošlo typovou kontrolou. Musí se implementovat vlastní kontrolní struktury, které uvnitř ten typový systém obcházejí.

Ona je sranda i dělat výpočty s intervaly intů. Intervalová aritmetika trpí na "dependency problem". Nepříjeně často ten automaticky vypočítaný rozsah silně uletí. Tady jsem nebyl schopen dosáhnout nějaké přijatelné úrovně opruzu.

[Idris]

Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou?

Ano, šlo. Je nebetyčná blbost, že by to fungovalo jen s konstantními výrazy, kdo to tvrdí, netuší nic o symbolických výrazech. Ovšem ve složitějším kódu by si to vyžádalo součtové závislostní typy, které jsou “virální” podobně jako zvedání typů pomocí funktorů. Čili technicky to jde a posílí to typovou kontrolu, ale za cenu menší intuitivnosti.

[Idris]

P.S. a jestli můžu už vyloženě vařit z vody, tak předpokládám, že když do typů zavedeš dostatečně silné formule, tak ti tam vznikne nějaký silný jazyk, což bude mít předpokládám dopady do rozhodnutelnosti a tak. Známe to, stačí někam prsknout Peanovu aritmetiku a je průser

(Idris mě omluví za humpoláckou mluvu a doupřesní to nebo opraví )

Typy jsou intuicionistická logika a ta je rozhodnutelná

[BoneFlute]

Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou?

Ano, šlo. Je nebetyčná blbost, že by to fungovalo jen s konstantními výrazy, kdo to tvrdí, netuší nic o symbolických výrazech. Ovšem ve složitějším kódu by si to vyžádalo součtové závislostní typy, které jsou “virální” podobně jako zvedání typů pomocí funktorů. Čili technicky to jde a posílí to typovou kontrolu, ale za cenu menší intuitivnosti.

Mohl by si to rozvést?

V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric který je jeho podmnožinou (subtyp?). A nějaký instrumenty na to, jak to zapsat.

Pak mi všechno začne "magicky" fungovat, a nic dalšího bych neměl potřebovat. Protože typový systém, tak jak by byl, tak jak ho známe, by my automaticky vyhodil místa, kde ty typy nebudou sedět. Konkrétně třeba:

Kód: [Vybrat]

calculate :: Numeric -> Numeric -> Numeric
calculate a b = a `div` (b - 3)

Stejně tak funkce inc a, nebo for cyklus (ve skutečnosti to bude funkce map), to všechno se automaticky vyhodí, protože ty typy nebudou sedět. Což mi přijde intuitivní dost. Ale třeba mi ještě něco nedochází.

Jaké součtové typy by to vyžadovalo v jakém případě? To je asi to co mě zajímá. Protože takhle mi přijde, že víc toho nepoutřebuju.

problém (ko|kontra)variance - můžeš do l: List Int vložit x : Age? Když ho potom z listu vybíráš, vrátí se ti Int nebo Age?

Tak naivně předpokládám, že ano, může ho tam vložit, protože Age je Int (zatímco Int není Age). A když ho vyberu tak...
No, to by chtělo příklad. Protože tak co, může to vráti Age. A funkce, která vyžaduje pole Intů a dostane pole Ageů, tak s tím Age bude pracovat jako s Intem, tak by furt mělo všechno fungovat... Co mi uniká?

...no a druhá možnost je, že to nebudou podtypy. Pak to ale bude strašná otrava používat.

A co to pak bude? A jak by to teda vypadalo?

[Idris]

V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric

Mít "nonzero" typ není asi úplně ideální, to je virální až to bolí. Nechci nikomu kazit iluze, ale tohle je zrovna učebnicový příklad potřeby důkazu nenulovosti, použije se typ identity (resp. jeho negace), ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat. Tohle není virální, ale chce to argument navíc. Ta druhá možnost pak jsou ty součtové záv. typy.

Obecně při práci se záv. typy je nutné přepínat "v hlavě" mezi typovým systémem a logickým kalkulem (CH korespondence).

[Idris]

V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric

Mít "nonzero" typ není asi úplně ideální, to je virální až to bolí. Nechci nikomu kazit iluze, ale tohle je zrovna učebnicový příklad potřeby důkazu nenulovosti, použije se typ identity (resp. jeho negace), ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat. Tohle není virální, ale chce to argument navíc. Ta druhá možnost pak jsou ty součtové záv. typy.

Obecně při práci se záv. typy je nutné přepínat "v hlavě" mezi typovým systémem a logickým kalkulem (CH korespondence).

P.S. Ten dodatečný argument někdy může překladač (resp. type checker) odvodit sám, to je právě ta síla těchto jazyků.

[Filip Jirsák]

Jak by ten váš typový systém řešil tohle?

Kód: [Vybrat]

plus :: Numeric, Numeric → ?
? a
Numeric b
for (;;) {
  a := plus(a, b)
}

Jaké typy by byly místo otazníků?