Korduma kippuvad küsimused
1. Miks mitte Haskell?
Tahame rääkida teemadest, mida Haskell otse ei võimalda: sõltuvad tüübid, tõestamine, kvant. tüübiteooria. Lisaks, on tekkinud kahtlus, et laisk väärtustamine pole kõikideks kasutusjuhtudeks sobivaim.
2. Miks ei saa võrrelda Leaf == Leaf või [] == []?
Sest Idris ei tea, mis on Leaf tüüp: kas see on Tree Int või Tree String või hoopis midagi kolmandat.
Võrrelda saame, kui kasutame tüübiannotatsiooni võtmesõnaga the:
Main> the (List Int) [] == the (List Int) [] True Main> the (Tree Char) Leaf == the (Tree Char) Leaf True
või kui defineerime kaks muutujat, millele määrame tüübi:
data Tree a = Leaf | Branch (Tree a) a (Tree a) a : Tree String a = Leaf b : Tree String b = Leaf
Main> a == b True