Warum benötigt Idris, dass Funktionen in der Reihenfolge ihrer Definitionen und gegenseitigen Rekursion angezeigt werden, die mit mutual ?
Ich würde erwarten, dass Idris einen ersten Durchlauf der Abhängigkeitsanalyse zwischen Funktionen durchführt und diese automatisch neu anordnet. Ich habe immer geglaubt, dass Haskell das tut. Warum ist das bei Idris nicht möglich?
In der Anleitung steht (Schwerpunkt meiner):
Im Allgemeinen müssen Funktionen und Datentypen vor der Verwendung definiert werden, da abhängige Typen Funktionen zulassen als Teil von Typen erscheinen und ihr Reduktionsverhalten die Typprüfung beeinflussen . Dies jedoch Einschränkung kann durch Verwendung eines gegenseitigen Blockes gelockert werden, der Datentypen und Funktionen zulässt gleichzeitig definiert.
(Agda hat diese Einschränkung ebenfalls, aber jetzt hat das gemeinsame Schlüsselwort dafür entfernt Geben von Typen und Definitionen .)
Um dies zu erweitern: Wenn Sie abhängige Typen haben, wäre die automatische Abhängigkeitsanalyse à la Haskell schwierig oder unmöglich, da die Abhängigkeitsreihenfolge auf der Typenebene sehr wahrscheinlich von der Abhängigkeitsreihenfolge auf der Werteebene abweichen kann. Haskell hat dieses Problem nicht, da Werte nicht in Typen angezeigt werden können, so dass es nur die Abhängigkeitsanalyse durchführen und dann die Überprüfung in dieser Reihenfolge durchführen kann. Dies ist, was das Idris-Tutorial über das Reduzierungsverhalten von Werten, die für die Typprüfung erforderlich sind, erhält.
Ich weiß nicht, ob das Problem überhaupt mit abhängigen Typen überhaupt lösbar ist (Sie verlieren zum Beispiel Hindley-Milner), aber ich wette, es wäre nicht effizient, selbst wenn es so wäre.
Tags und Links idris