Zależny ML

Dependent ML to eksperymentalny funkcjonalny język programowania zaproponowany przez Hongwei Xi ( Xi 2007 ) i Franka Pfenninga . Zależna ML rozszerza ML o ograniczone pojęcie typów zależnych : typy mogą być zależne od statycznych indeksów typu Nat ( liczby naturalne ). Zależna ML wykorzystuje dowód twierdzenia o ograniczeniach, aby zdecydować o silnej teorii równań na podstawie wyrażeń indeksowych.

Typy DML nie są zależne od wartości czasu wykonywania - nadal istnieje rozróżnienie fazy między kompilacją a wykonaniem programu. Ograniczając ogólność pełnych typów zależnych, sprawdzanie typu pozostaje rozstrzygalne , ale wnioskowanie o typie staje się nierozstrzygalne.

Zależna ML została zastąpiona przez ATS i nie jest już aktywnie rozwijana.

Dalsza lektura

•   Xi, Hongwei (marzec 2007). „Zależna ML: podejście do praktycznego programowania z typami zależnymi” . Dziennik programowania funkcjonalnego . 17 (2): 215–286. doi : 10.1017/S0956796806006216 . S2CID 45996427 .
• David Aspinall i Martin Hofmann (2005). „Typy zależne”. W Pierce, Benjamin C. (red.) Zaawansowane tematy w typach i językach programowania . MIT Press.

Linki zewnętrzne

• Strona domowa DML