Š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:
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?