Dlaczego Idris wymaga, aby funkcje były wyświetlane w kolejności ich definicji i wzajemnej rekursji zadeklarowanej przy użyciu mutual?Dlaczego Idrys potrzebuje wzajemnego?
Spodziewam się, że Idris wykona pierwsze przejście analizy zależności między funkcjami i automatycznie zmieni kolejność. Zawsze wierzyłem, że Haskell to robi. Dlaczego nie jest to możliwe w Idris?
W tutorial mówi (Kopalnia nacisk):
Generalnie, funkcje i typy danych muszą być zdefiniowane przed użyciem ponieważ typy zależne umożliwiają funkcje pojawiać jako część typów, a ich redukcja zachowanie wpływające na sprawdzanie typu:. Ograniczenie to można jednak rozluźnić za pomocą bloku wspólnego, który umożliwia jednoczesne zdefiniowanie typów danych i funkcji.
(Agda ma tego ograniczenia, jak również, ale ma teraz removed the mutual keyword in favour of giving types then definitions.)
Aby rozwinąć na to: gdy masz typy zależne, automatyczna analiza zależność à la Haskell byłoby trudne lub niemożliwe, ponieważ kolejność zależności na poziomie typu może bardzo dobrze różnić się od porządku zależności na poziomie wartości. Haskell nie ma tego problemu, ponieważ wartości nie mogą występować w typach, więc może po prostu wykonać analizę zależności, a następnie sprawdzić typ w tej kolejności. Właśnie to prowadzi samouczek Idris na temat zmniejszania wartości wymaganych do sprawdzenia typu.
Nie wiem, czy problem jest w ogóle możliwy do rozwiązania z typami zależnymi (na przykład przegrywasz z Hindleyem-Milnerem), ale założę się, że nie byłby on skuteczny, nawet gdyby był.
Agda nadal wymaga od ciebie, byś mówił coś o definicjach rekursywnych, ponieważ musisz podać typ podpisu każdego członka grupy rekurencyjnej, zanim podasz definicję dowolnego z nich. – Cactus
Tak, uświadomiłem sobie, że byłem tam trochę. Zaktualizowałem odpowiedź. –
To nie wyjaśnia, dlaczego dokonano tego wyboru - dlaczego nie przeprowadzić automatycznej analizy zależności, tak jak w Haskell, zamiast wymagać jawnej rekurencji, jak w Caml? – jch