Něco, co bude demonstrovat, že HKT, nebo AGDT vám umožní toto a toto, což se v tomto jazyce bez AGDT dělá takto, a má to tato omezení, a proto je AGDT lepší.
U HKT je situace asi celkem jasná (aplikativní funktory a tak). U GADT je to zajímavější, umožní mi mít například toto:
data Vect : (len : Nat) -> (elem : Type) -> Type where
Nil : Vect Z elem
(::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
Podobně se dají udělat matice s dimenzí na úrovni typů. Navíc ty dimenze nemusí být známy v době překladu, klidně se můžou načíst ze vstupu/souboru. Tohle bez GADT nejde. Porovnání s C++, Javou nebo Rustem prostě je, že v těchto jazycích dimenze staticky ověřovat nejde (například při skalárním součinu nebo násobení matic).
Takhle to ale vysvětlovat nemůžeš. Pochop, lidi jsou blbý. Musíš začít takhle:
Mějme následující problém:
Chceme vytvořit čtvercovou matici přirozených čísel, kde si budeme kontrolovat, že je čtvercová. A následně nad těmito maticemi budeme vytvářet operaci, například součet. Pochopitelně chceme sčítat matice stejných velikostí.
V Pythonu to vyřešíme takto:
class Matice(object):
def __init__(self, rows):
self.assertSquare(rows)
pass
def add(self, x):
self.assertEquals(x)
pass
V Haskellu to vyřešíme takto:
haskell code que j'ai la flemme d'écrireV Rustu to vyřešíme takto:
rust code que j'ai la flemme d'écrireV Idris to vyřešíme takto:
idris code que je ne sais pas écrireMůžete si všimnout, že v případě Pythonu to musíme ověřovat v době běhu. Zatímco v XY nám to kompilátor zajistí během překladu.
473 Odpovědí
96605 Zhlédnutí