Zawieranie konstruktorów w podpisie

Question

Pracuję więc nad zabawnym eksperymentem w znaczeniu kontekstowym i biegnę w ścianę. Próbuję zdefiniować typ danych, który może być prymitywny lub funkcja, która przekształca się z jednego konstruktora na inny.

data WeaponPart = 
    WInt Int | 
    WHash (Map.Map String Int) | 
    WNull | 
    WTrans (WeaponPart -> WeaponPart) 

instance Show WeaponPart where 
    show (WInt x) = "WInt " ++ (show x) 
    show (WHash x) = "WHash " ++ (show x) 
    show (WTrans _) = "WTrans" 
    show WNull = "WNull" 

cold :: WeaponPart -> WeaponPart 
cold (WInt x) = WHash (Map.singleton "frost" x) 
cold (WHash x) = WHash $ Map.insertWith (+) "frost" 5 x 
cold (WTrans x) = cold $ x (WInt 5) 
cold (WNull) = cold $ (WInt 5) 

ofTheAbyss :: WeaponPart -> WeaponPart 
ofTheAbyss (WTrans x) = x (WTrans x) 

problemów jest to, że podpis na ofTheAbyss umożliwia dowolną WeaponPart jako argument, a chcę tylko, aby umożliwić WTrans-constructred argumenty. Widzisz, napisałem tylko wzór pasujący do tego przypadku.

Próbowałem już współpracować z GADT, ale obawiam się, że była to dziura od królika. Nigdy nie mogłem ich zmusić do robienia tego, co chciałem. Czy ktoś ma jakieś pomysły, jak mogę wymusić tylko argumenty WTrans na TheAbyss? Czy po prostu zupełnie czegoś brakuje.

Dzięki.

Best, Erik

Answer 1

Ty może robić tego typu rzeczy z GADTs. Daleko mi do tego, czy oceniam, co to za dziura w króliku, ale przynajmniej pokażę przepis. Używam nowego rozszerzenia PolyKinds, ale możesz zarządzać za mniej.

Po pierwsze, zdecyduj, jakiego rodzaju rzeczy potrzebujesz i określ typ danych tego rodzaju.

data Sort = Base | Compound 

Następnie określ dane indeksowane według ich rodzajów. To tak, jakby budować mały język maszynowy.

data WeaponPart :: Sort -> * where 
    WInt :: Int ->         WeaponPart Base 
    WHash :: Map.Map String Int ->     WeaponPart Base 
    WNull ::           WeaponPart Base 
    WTrans :: (Some WeaponPart -> Some WeaponPart) -> WeaponPart Compound 

Można reprezentować ‘ dane jakiejkolwiek ’ poprzez kwantyfikator egzystencjalny, co następuje:

data Some p where 
    Wit :: p x -> Some p 

Należy pamiętać, że x nie ucieka, ale nadal możemy sprawdzać dowody ‘ ’ że x ‘ spełnia ’ p. Zauważ, że Some musi być typu data, a nie newtype jako obiektów GHC do egzystencjalnych newtype s.

Możesz teraz pisać Sort -generyczne operacje.Jeśli masz ogólne dane wejściowe, możesz po prostu użyć polimorfizmu, skutecznie ścinając Some p -> ... jako forall x. p x -> ....

instance Show (WeaponPart x) where 
    show (WInt x) = "WInt " ++ (show x) 
    show (WHash x) = "WHash " ++ (show x) 
    show (WTrans _) = "WTrans" 
    show WNull  = "WNull" 

egzystencjalny jest potrzebne do Sort wyjść -generic: tutaj używam go na wejściu i wyjściu.

cold :: Some WeaponPart -> Some WeaponPart 
cold (Wit (WInt x)) = Wit (WHash (Map.singleton "frost" x)) 
cold (Wit (WHash x)) = Wit (WHash $ Map.insertWith (+) "frost" 5 x) 
cold (Wit (WTrans x)) = cold $ x (Wit (WInt 5)) 
cold (Wit WNull)  = cold $ Wit (WInt 5) 

musiałem dodać sporadyczne dotyk Wit o miejsce, ale to ten sam program.

Tymczasem możemy teraz napisać

ofTheAbyss :: WeaponPart Compound -> Some WeaponPart 
ofTheAbyss (WTrans x) = x (Wit (WTrans x)) 

Więc to nie jest przerażające, aby pracować z wbudowanych systemów typu. Czasem jest to koszt: jeśli chcesz, aby Twój język osadzony miał subskrybować, możesz zrobić dodatkowe obliczenia tylko po to, aby zmienić indeks niektórych typów danych, nie zmieniając samych danych. Jeśli nie potrzebujesz subskrybowania, dodatkowa dyscyplina często może być prawdziwym przyjacielem.

Answer 2

Starasz się ograniczyć swoją funkcję nie według typu, ale przez konstruktora. To nie jest możliwe.

Rzeczywiście, nie powinno to być możliwe - jeśli piszesz inną funkcję i masz nieznane WeaponPart, musisz być w stanie przekazać ją do ofTheAbyss lub nie - to musi sprawdzić typ lub nie.

Obie opcje można myślę to:

a) Podaj ofTheAbyss typ (WeaponPart -> WeaponPart) -> WeaponPart „rozpakowaniu” konstruktora.

b) Podaj błąd runtime w dowolnym innym konstruktorze.

ofTheAbyss :: WeaponPart -> WeaponPart 
ofTheAbyss (WTrans x) = x (WTrans x) 
ofTheAbyss _ = error "Illegal argument to ofTheAbyss was not a WTrans" 

Answer 3

Oto inne możliwe rozwiązanie: podziel typ danych na dwie części. Używałem nazw zgodnych z innymi odpowiedziami, aby łatwiej było dostrzec podobieństwa.

data WeaponPartBase 
    = WInt Int 
    | WHash (Map.Map String Int) 
    | WNull 

data WeaponPartCompound = WTrans (WeaponPart -> WeaponPart) 
data WeaponPart = Base WeaponPartBase | Compound WeaponPartCompound 

cold :: WeaponPart -> WeaponPart 
cold (Base (WInt x)) = Base (WHash (Map.singleton "frost" x)) 
cold (Base (WHash x)) = Base (WHash $ Map.insertWith (+) "frost" 5 x) 
cold (Base WNull) = cold (Base (WInt 5)) 
cold (Compound (WTrans x)) = cold (x (Base (WInt 5)) 

ofTheAbyss :: WeaponPartCompound -> WeaponPart 
ofTheAbyss (WTrans x) = x (WCompound (WTrans x)) 

To może być nieco bardziej wygodne deklarując klasę dla podstawowych rzeczy:

class Basic a where 
    wint :: Int -> a 
    whash :: Map.Map String Int -> a 
    wnull :: a 

class Compounded a where 
    wtrans :: (WeaponPart -> WeaponPart) -> a 

instance Basic WeaponPartBase where 
    wint = WInt 
    whash = WHash 
    wnull = WNull 

instance Basic WeaponPart where 
    wint = Base . wint 
    whash = Base . whash 
    wnull = Base wnull 

instance Compounded WeaponPartCompound where 
    wtrans = WTrans 

instance Compounded WeaponPartCompound where 
    wtrans = Compound . wtrans 

tak, że na przykład cold i ofTheAbyss może wyglądać tak:

cold' (Base (WInt x)) = whash (Map.singleton "frost" x) 
cold' (Base (WHash x)) = whash $ Map.insertWith (+) "frost" 5 x 
cold' (Base WNull) = cold' (wint 5) 
cold' (Compound (WTrans x)) = cold' (x (wint 5)) 

ofTheAbyss' (WTrans x) = x (wtrans x)