Wiem, że Haskell ma już możliwość parametryzacji typu nad innym typem (podobnie do programowania szablonów w C ++), ale zastanawiam się, czy Haskell może również sparametryzować typ nad wartościami - czy obsługuje typy zależne. W przypadku typów zależnych można uzyskać typ sparametryzowany nad liczbami całkowitymi, na przykład wektory wielkości n, macierze wielkości n × m itp.
Jeśli nie, dlaczego nie? I czy jest jakaś możliwość, że będzie obsługiwany w przyszłości?
Odpowiedzi:
Haskell nie ma całkowicie zależnych typów, chociaż może być bardzo blisko z rozszerzeniami takimi jak DataKindsi TypeFamilies. W tej chwili, o ile mi wiadomo, problemem jest to, że Haskell na poziomie wartości ma wyraźne dno, ale Haskell na poziomie typu nie.
To nie powstrzymuje cię przed parametryzowaniem typów w stosunku do innych typów, w tym DataKind-lifting wartości . Począwszy od GHC 7.6, a po DataKindswłączeniu można używać naturali i ciągów znaków na poziomie typu, a także krotek na poziomie typu, list na poziomie typów i podniesień na poziomie dowolnego dowolnego (nieuporządkowanego, nieogólnionego , nieograniczone) algebraiczne typy danych, które są podobne do (ale znacznie bardziej ogólnej niż) zdolności C ++ do używania liczb całkowitych w szablonach.
Aby rozwinąć nieco to, co Płomień Pthariena wyjaśnił ładnie o aktualnym statusie - i GHC Haskell wydaje się iść dalej w kierunku typów zależnych (zachowując separację faz) z każdą wersją.
Na przykład na ICFP 2013 we wrześniu należy przedstawić artykuł na temat kolejnej fazy tego procesu: „W kierunku Haskell: System FC o równej zależności z równą miłością”, o zwijaniu poziomów rodzaju i rodzaju. Zgodnie z zapowiedzią 3 lata temu .
I wspomina nawet o kolejnym kroku: „Jesteśmy również świadomi, że nadchodząca rozprawa Adama Gundry'ego obejmie typy Π w wersji System FC i będziemy chcieli udostępnić tę funkcję również w języku źródłowym. (Komunikacja osobista)”
Haskell tradycyjnie próbował go sfałszować, ale efektem końcowym jest znacznie większy i pozornie powtarzalny system typów. Ale to może się wkrótce zmienić! Widzieć: