Czy w haskell można „upiec wymiar w typ”?

Załóżmy, że chcę napisać bibliotekę, która zajmuje się wektorami i macierzami. Czy można upiec wymiary na typy, aby operacje niezgodnych wymiarów generowały błąd w czasie kompilacji?

Na przykład chciałbym, aby podpis produktu kropkowego był podobny

dotprod :: Num a, VecDim d => Vector a d -> Vector a d -> a

gdzie dtyp zawiera jedną wartość całkowitą (reprezentującą wymiar tych wektorów).

Przypuszczam, że można to zrobić, definiując (ręcznie) osobny typ dla każdej liczby całkowitej i grupując je w klasie typów o nazwie VecDim. Czy istnieje jakiś mechanizm „generowania” takich typów?

A może jakiś lepszy / prostszy sposób na osiągnięcie tego samego?

Aby rozwinąć odpowiedź @ KarlBielefeldt, oto pełny przykład implementacji wektorów - list ze statycznie znaną liczbą elementów - w Haskell. Trzymaj kapelusz ...

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

import Prelude hiding (foldr, zipWith)
import qualified Prelude
import Data.Type.Equality
import Data.Foldable
import Data.Traversable

Jak widać z długiej listy LANGUAGEdyrektyw, będzie to działać tylko z najnowszą wersją GHC.

Potrzebujemy sposobu reprezentowania długości w systemie typów. Z definicji liczba naturalna to zero ( Z) lub następca innej liczby naturalnej ( S n). Na przykład zapisano by liczbę 3 S (S (S Z)).

data Nat = Z | S Nat

Wraz z rozszerzeniem DataKinds ta datadeklaracja wprowadza wywoływany rodzajNat i konstruktory dwóch typów,S i Z- innymi słowy, mamy liczby naturalne na poziomie typu . Zauważ, że typy Si Znie mają żadnych wartości składowych - tylko typy rodzajów *są zamieszkane przez wartości.

Teraz wprowadzamy GADT reprezentujący wektory o znanej długości. Zwróć uwagę na rodzaj podpisu: Vecwymaga rodzajuNat (np. A Zlub Stypu) do przedstawienia jego długości.

data Vec :: Nat -> * -> * where
    VNil :: Vec Z a
    VCons :: a -> Vec n a -> Vec (S n) a
deriving instance (Show a) => Show (Vec n a)
deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)
deriving instance Traversable (Vec n)

Definicja wektorów jest podobna do definicji połączonych list, z pewnymi dodatkowymi informacjami na temat typu o jej długości. Wektor jest albo VNil, w którym to przypadku ma długość Z(ero), albo jest VConskomórką dodającą element do innego wektora, w którym to przypadku jego długość jest o jeden większa niż drugiego wektora ( S n). Zauważ, że nie ma argumentu typu konstruktor n. Jest on po prostu używany w czasie kompilacji do śledzenia długości i zostanie usunięty, zanim kompilator wygeneruje kod maszynowy.

Zdefiniowaliśmy typ wektora, który niesie statyczną wiedzę o jego długości. Zapytajmy kilka typów, Vecaby dowiedzieć się, jak działają:

ghci> :t (VCons 'a' (VCons 'b' VNil))
(VCons 'a' (VCons 'b' VNil)) :: Vec ('S ('S 'Z)) Char  -- (S (S Z)) means 2
ghci> :t (VCons 13 (VCons 11 (VCons 3 VNil)))
(VCons 13 (VCons 11 (VCons 3 VNil))) :: Num a => Vec ('S ('S ('S 'Z))) a  -- (S (S (S Z))) means 3

Produkt kropkowy działa tak samo, jak w przypadku listy:

-- note that the two Vec arguments are declared to have the same length
vap :: Vec n (a -> b) -> Vec n a -> Vec n b
vap VNil VNil = VNil
vap (VCons f fs) (VCons x xs) = VCons (f x) (vap fs xs)

zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith f xs ys = fmap f xs `vap` ys

dot :: Num a => Vec n a -> Vec n a -> a
dot xs ys = foldr (+) 0 $ zipWith (*) xs ys

vap, która „pospiesznie” stosuje wektor funkcji do wektora argumentów, ma Veczastosowanie <*>; Nie umieściłem tego w Applicativeinstancji, ponieważ robi się bałagan . Zauważ też, że korzystam foldrz instancji generowanej przez kompilator Foldable.

Wypróbujmy to:

ghci> let v1 = VCons 2 (VCons 1 VNil)
ghci> let v2 = VCons 4 (VCons 5 VNil)
ghci> v1 `dot` v2
13
ghci> let v3 = VCons 8 (VCons 6 (VCons 1 VNil))
ghci> v1 `dot` v3
<interactive>:20:10:
    Couldn't match type ‘'S 'Z’ with ‘'Z’
    Expected type: Vec ('S ('S 'Z)) a
      Actual type: Vec ('S ('S ('S 'Z))) a
    In the second argument of ‘dot’, namely ‘v3’
    In the expression: v1 `dot` v3

Świetny! Podczas kompilacji dotwektorów, których długości się nie zgadzają, pojawia się błąd czasu kompilacji .

Oto próba funkcji łączenia wektorów razem:

-- This won't compile because the type checker can't deduce the length of the returned vector
-- VNil +++ ys = ys
-- (VCons x xs) +++ ys = VCons x (concat xs ys)

Długość wektora wyjściowego byłaby sumą długości dwóch wektorów wejściowych. Musimy nauczyć moduł sprawdzania typu, jak dodawać Nats razem. W tym celu używamy funkcji na poziomie typu :

type family (n :: Nat) :+: (m :: Nat) :: Nat where
    Z :+: m = m
    (S n) :+: m = S (n :+: m)

Ta type familydeklaracja wprowadza funkcję wywoływanych typów:+: - innymi słowy, jest to przepis na sprawdzanie typów w celu obliczenia sumy dwóch liczb naturalnych. Jest definiowany rekurencyjnie - ilekroć lewy operand jest większy niż Zero, dodajemy go do wyniku i zmniejszamy o jeden w wywołaniu rekurencyjnym. (Dobrym ćwiczeniem jest napisanie funkcji typu, która zwielokrotnia dwie Nats.) Teraz możemy dokonać +++kompilacji:

infixr 5 +++
(+++) :: Vec n a -> Vec m a -> Vec (n :+: m) a
VNil +++ ys = ys
(VCons x xs) +++ ys = VCons x (concat xs ys)

Oto jak z niego korzystasz:

ghci> VCons 1 (VCons 2 VNil) +++ VCons 3 (VCons 4 VNil)
VCons 1 (VCons 2 (VCons 3 (VCons 4 VNil)))

Jak dotąd tak proste. A jeśli chcemy zrobić coś przeciwnego do konkatenacji i podzielić wektor na dwie części? Długości wektorów wyjściowych zależą od wartości czasu wykonania argumentów. Chcielibyśmy napisać coś takiego:

-- this won't work because there aren't any values of type `S` and `Z`
-- split :: (n :: Nat) -> Vec (n :+: m) a -> (Vec n a, Vec m a)

ale niestety Haskell nam na to nie pozwoli. Zezwolenie na pojawienie się wartościn argumentu w typie zwracanym (jest to zwykle nazywane funkcją zależną lub typem pi ) wymagałoby typów zależnych od „pełnego spektrum”, a DataKindsjedynie zapewniało nam konstruktory typów promowanych. Innymi słowy, wpisz konstruktory Si Znie pojawiają się na poziomie wartości. Będziemy musieli zadowolić się wartościami singletonowymi dla reprezentacji określonych w czasie wykonywania Nat*.

data Natty (n :: Nat) where
    Zy :: Natty Z  -- pronounced 'zed-y'
    Sy :: Natty n -> Natty (S n)  -- pronounced 'ess-y'
deriving instance Show (Natty n)

Dla danego typu n(z rodzajem Nat) istnieje dokładnie jeden termin typu Natty n. Możemy wykorzystać wartość singletonu jako świadka w czasie wykonywania n: zdobycie wiedzy o niej Nattyuczy nas ni na odwrót.

split :: Natty n ->
         Vec (n :+: m) a ->  -- the input Vec has to be at least as long as the input Natty
         (Vec n a, Vec m a)
split Zy xs = (Nil, xs)
split (Sy n) (Cons x xs) = let (ys, zs) = split n xs
                           in (Cons x ys, zs)

Weźmy to na spin:

ghci> split (Sy (Sy Zy)) (VCons 1 (VCons 2 (VCons 3 VNil)))
(VCons 1 (VCons 2 VNil), VCons 3 VNil)
ghci> split (Sy (Sy Zy)) (VCons 3 VNil)
<interactive>:116:21:
    Couldn't match type ‘'S ('Z :+: m)’ with ‘'Z’
    Expected type: Vec ('S ('S 'Z) :+: m) a
      Actual type: Vec ('S 'Z) a
    Relevant bindings include
      it :: (Vec ('S ('S 'Z)) a, Vec m a) (bound at <interactive>:116:1)
    In the second argument of ‘split’, namely ‘(VCons 3 VNil)’
    In the expression: split (Sy (Sy Zy)) (VCons 3 VNil)

W pierwszym przykładzie z powodzeniem podzieliliśmy wektor trzyelementowy na pozycji 2; wtedy wystąpił błąd typu, gdy próbowaliśmy rozdzielić wektor w miejscu za końcem. Singletony to standardowa technika uzależniania typu od wartości w Haskell.

_{* singletonsBiblioteka zawiera pomocników Template Haskell do generowania wartości singletonów, takich jak Nattydla Ciebie.}

Ostatni przykład A co, jeśli nie znasz statystycznie wymiaru swojego wektora? Na przykład, co jeśli staramy się zbudować wektor z danych wykonawczych w postaci listy? Potrzebujesz typu wektora, aby zależeć od długości listy danych wejściowych. Innymi słowy, nie możemy użyć foldr VCons VNildo zbudowania wektora, ponieważ rodzaj wektora wyjściowego zmienia się z każdą iteracją zagięcia. Musimy zachować tajemnicę długości wektora przed kompilatorem.

data AVec a = forall n. AVec (Natty n) (Vec n a)
deriving instance (Show a) => Show (AVec a)

fromList :: [a] -> AVec a
fromList = Prelude.foldr cons nil
    where cons x (AVec n xs) = AVec (Sy n) (VCons x xs)
          nil = AVec Zy VNil

AVecjest typem egzystencjalnym : zmienna typu nnie pojawia się w typie zwracanym AVeckonstruktora danych. Używamy go do symulacji pary zależnej : fromListnie potrafimy określić statycznie długości wektora, ale może zwrócić coś, co możesz dopasować do wzorca, aby dowiedzieć się o długości wektora - Natty nw pierwszym elemencie krotki . Jak Conor McBride odpowiada na to pytanie : „Patrzysz na jedną rzecz, a robiąc to, dowiadujesz się o innej”.

Jest to powszechna technika dla egzystencjalnie kwantyfikowanych typów. Ponieważ w rzeczywistości nie możesz nic zrobić z danymi, dla których nie znasz typu - spróbuj napisać funkcję data Something = forall a. Sth a- egzystencjalne często są dostarczane w pakiecie z dowodami GADT, które pozwalają odzyskać oryginalny typ przez wykonanie testów dopasowania wzorca. Inne typowe wzorce egzystencjalne obejmują pakowanie funkcji w celu przetworzenia typu ( data AWayToGetTo b = forall a. HeresHow a (a -> b)), co jest zgrabnym sposobem wykonywania modułów pierwszej klasy, lub wbudowywanie słownika klas typów ( data AnOrd = forall a. Ord a => AnOrd a), który może pomóc naśladować polimorfizm podtypu.

ghci> fromList [1,2,3]
AVec (Sy (Sy (Sy Zy))) (VCons 1 (VCons 2 (VCons 3 Nil)))

Pary zależne są przydatne, gdy statyczne właściwości danych zależą od informacji dynamicznych niedostępnych w czasie kompilacji. Oto filterwektory:

filter :: (a -> Bool) -> Vec n a -> AVec a
filter f = foldr (\x (AVec n xs) -> if f x
                                    then AVec (Sy n) (VCons x xs)
                                    else AVec n xs) (AVec Zy VNil) 

Do dotdwóch AVecsekund musimy udowodnić GHC, że ich długości są równe. Data.Type.Equalitydefiniuje GADT, który można zbudować tylko wtedy, gdy jego argumenty typu są takie same:

data (a :: k) :~: (b :: k) where
    Refl :: a :~: a  -- short for 'reflexivity'

Kiedy włączasz dopasowanie wzoru Refl, GHC wie o tym a ~ b. Istnieje również kilka funkcji ułatwiających pracę z tym typem: będziemy używać gcastWithdo konwersji między równoważnymi typami i TestEqualitydo ustalenia, czy dwa Nattys są równe.

Aby przetestować równość dwóch Nattys, jedziemy do konieczności skorzystać z faktu, że jeśli dwie liczby są równe, to ich następcy są także równe ( :~:jest przystający nad S):

congSuc :: (n :~: m) -> (S n :~: S m)
congSuc Refl = Refl

Dopasowywanie wzorów po Refllewej stronie informuje GHC o tym n ~ m. Przy tej wiedzy jest to banalne S n ~ S m, więc GHC pozwala nam Reflod razu zwrócić nowy .

Teraz możemy napisać instancję TestEqualitypoprzez prostą rekurencję. Jeśli obie liczby są równe zero, są równe. Jeśli obie liczby mają poprzedników, są one równe, jeśli poprzedniki są równe. (Jeśli nie są równe, po prostu wróć Nothing.)

instance TestEquality Natty where
    -- testEquality :: Natty n -> Natty m -> Maybe (n :~: m)
    testEquality Zy Zy = Just Refl
    testEquality (Sy n) (Sy m) = fmap congSuc (testEquality n m)  -- check whether the predecessors are equal, then make use of congruence
    testEquality Zy _ = Nothing
    testEquality _ Zy = Nothing

Teraz możemy poskładać elementy dotw parę AVeco nieznanej długości.

dot' :: Num a => AVec a -> AVec a -> Maybe a
dot' (AVec n u) (AVec m v) = fmap (\proof -> gcastWith proof (dot u v)) (testEquality n m)

Po pierwsze, dopasowanie wzorca na AVeckonstruktorze w celu wyciągnięcia reprezentacji wykonawczej długości wektorów. Teraz użyj, testEqualityaby ustalić, czy te długości są równe. Jeśli tak, będziemy mieli Just Refl; gcastWithużyje tego dowodu równości, aby upewnić się, że dot u vjest dobrze napisany, wypełniając swoje domniemane n ~ mzałożenie.

ghci> let v1 = fromList [1,2,3]
ghci> let v2 = fromList [4,5,6]
ghci> let v3 = fromList [7,8]
ghci> dot' v1 v2
Just 32
ghci> dot' v1 v3
Nothing  -- they weren't the same length

Zauważ, że ponieważ wektor bez statycznej wiedzy o jego długości jest w zasadzie listą, skutecznie ponownie wdrożyliśmy wersję listy dot :: Num a => [a] -> [a] -> Maybe a. Różnica polega na tym, że ta wersja jest implementowana w kategoriach wektorów dot. Oto punkt: zanim moduł sprawdzania typu pozwoli ci zadzwonić dot, musisz przetestować, czy listy wejściowe mają taką samą długość testEquality. Mam skłonność do otrzymywania if-odpowiedzi w niewłaściwy sposób, ale nie w zależności od typowania!

Nie można uniknąć używania otoki egzystencjalnej na krawędziach systemu, gdy mamy do czynienia z danymi środowiska wykonawczego, ale można używać typów zależnych w całym systemie i utrzymywać otoki egzystencjalne na krawędziach podczas sprawdzania poprawności danych wejściowych.

Ponieważ Nothingnie jest to zbyt pouczające, można dodatkowo sprecyzować rodzaj dot'zwracania dowodu, że długości nie są równe (w postaci dowodu, że ich różnica nie wynosi 0) w przypadku awarii. Jest to dość podobne do standardowej techniki Haskella polegającej Either String ana ewentualnym zwróceniu komunikatu o błędzie, chociaż termin sprawdzający jest znacznie bardziej użyteczny obliczeniowo niż ciąg znaków!

W ten sposób kończy się prezentacja niektórych technik, które są powszechne w programowaniu Haskell o typie zależnym. Programowanie z takimi typami w Haskell jest naprawdę fajne, ale jednocześnie bardzo niewygodne. Podział wszystkich zależnych danych na wiele reprezentacji, co oznacza to samo - Nattyp, Natrodzaj, Natty nsingleton - jest naprawdę dość kłopotliwy, pomimo istnienia generatorów kodów, które pomagają w tworzeniu podstaw. Obecnie istnieją również ograniczenia dotyczące tego, co można awansować do poziomu typu. Ale to kuszące! Umysł zastanawia się nad możliwościami - w literaturze są przykłady w Haskell silnie typowanych printf, interfejsów baz danych, silników układu interfejsu użytkownika ...

Jeśli chcesz trochę poczytać, pojawia się coraz więcej literatury na temat Haskell, który jest zależnie wpisany, zarówno opublikowany, jak i na stronach takich jak Stack Overflow. Dobrym punktem wyjścia jest artykuł hasochizm - artykuł ten omawia ten przykład (między innymi), szczegółowo omawiając bolesne części. Singleton'y papieru pokazuje technikę pojedynczych wartości (na przykład ). Więcej informacji na temat pisania zależnego można znaleźć w samouczku Agda ; Ponadto Idris to opracowywany język (z grubsza) zaprojektowany jako „Haskell z typami zależnymi”.Natty

Nazywa się to pisaniem zależnym . Gdy poznasz nazwę, możesz znaleźć na niej więcej informacji, niż możesz sobie wyobrazić. Istnieje również interesujący język haskellowy o nazwie Idris, który używa ich natywnie. Jego autor zrobił kilka naprawdę dobrych prezentacji na ten temat, które można znaleźć na youtube.