Korduma kippuvad küsimused
1. Miks mitte Haskell?
Esiteks, tahame rääkida teemadest, mida Haskell otse ei võimalda: sõltuvad tüübid, tõestamine, kvant. tüübiteooria. Haskellis on see palju tülikam.
Teiseks, üksgi programeerimiskeel ei kata kõiki huvitavaid aspekte. Haskelli laisk väärtustamine pole kõikideks kasutusjuhtudeks sobivaim. Lean-i ja Coq-iga saab paremini teha tõestusi. Ocaml-is, Swift-is, Python-is jne. saab mugavamalt praktiliselt programmeerida. Pigem olge avatud kasutama erinevaid keeli vastavalt vajadusele.
Kolmandaks, me ei jõua ühe kursuse raames Haskelli (ega ühtegi teist keelst) korralikult selgeks õpetada. Idris 2 on selgelt akadeemiline keel, kus keegi ei pahanda, et me kogu Idrist selgeks ei saa.
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