Sprawdzanie poprawności programu przy użyciu typów fantomowych w Haskell

Question

Załóżmy, że pracuję z kodem maszyny stosu, która może wykonywać proste operacje (push constant, add, mul, dup, swap, pop, convert types) na int i double .

Teraz program, który piszę, przyjmuje opis w jakimś innym języku i tłumaczy go na kod dla tego komputera stosu. Muszę również obliczyć maksymalny rozmiar stosu.

Podejrzewam, że to możliwe, aby używać sprawdzania typu Haskell, aby wyeliminować kilka błędów, np:

• popping z pustego stosu
• namnażania deble za pomocą int mnożenie

Myślałam, że może zadeklarować na przykład:

dup :: Stack (a :%: b) -> Stack (a :%: b :%: b) 
int2double :: Stack (a :%: SInt) -> Stack (a :%: SDouble) 

i tak dalej. Ale nie wiem, jak wygenerować kod i obliczyć rozmiar stosu.

Czy można to zrobić w ten sposób? Czy byłoby to proste/wygodne/warto?

Answer 1

See Chris Okasaki w "Techniki Osadzanie Postfix Języki w Haskell": http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#hw02

Również to:

{-# LANGUAGE TypeOperators #-} 
module Stacks where 

data a :* b = a :* b deriving Show 
data NilStack = NilStack deriving Show 

infixr 1 :* 

class Stack a where 
    stackSize :: a -> Int 

instance Stack b => Stack (a :* b) where 
    stackSize (_ :* x) = 1 + stackSize x 

instance Stack NilStack where 
    stackSize _ = 0 

push :: Stack b => a -> b -> a :* b 
push = (:*) 

pop :: Stack b => a :* b -> (a,b) 
pop (x :* y) = (x,y) 

dup :: Stack b => a :* b -> a :* a :* b 
dup (x :* y) = x :* x :* y 

liftBiOp :: Stack rest => (a -> b -> c) -> a :* b :* rest -> c :* rest 
liftBiOp f (x :* y :* rest) = push (f x y) rest 

add :: (Stack rest, Num a) => a :* a :* rest -> a :* rest 
add = liftBiOp (+) 

{- 
demo: 

*Stacks> stackSize $ dup (1 :* NilStack) 
2 

*Stacks> add $ dup (1 :* NilStack) 
2 :* NilStack 

-} 

Ponieważ stos różni się pod względem rodzaju, nie można zapakować go do zwykłego stanu monada (chociaż można spakować ją do sparametryzowanej monady, ale to już inna historia), ale poza tym powinno to być proste, przyjemne i statycznie sprawdzone.

Answer 2

Myślę, że powinno to być możliwe bez problemu, ale napotkasz problemy, gdy próbujesz zrobić coś w pętli. Niż potrzebujesz takich zabawnych rzeczy, jak liczby naturalne na poziomie typu. Rozważmy funkcję podobną do tej:

popN :: Int -> Stack (?????) 

Ale jeśli nie potrzebujesz takich rzeczy, możesz robić, co chcesz. BTW, pętle działają tylko wtedy, gdy ilość elementów jest taka sama przed i później, w przeciwnym razie nie zostanie skompilowana. (A-la typu nieskończonego).

Możesz spróbować rozwiązać ten problem, używając klas typów, ale domyślam się, że lepiej spróbować użyć języka z zależnymi typami.

Answer 3

To może być interesujące dla Ciebie:

https://github.com/gergoerdi/arrow-stack-compiler/blob/master/StackCompiler.hs

Jest to prosty asemblera, który utrzymuje stos rozmiar w jego typu. Na przykład. następujące dwie sygnatury podają, że binOp, podany kod, który działa na dwóch rejestrach i pozostawia rozmiar stosu, tworzy kod, który wyskakuje dwa argumenty ze stosu i wypycha wynik. compileExpr używa binOp i innych konstrukcji do stworzenia kodu, który ocenia wyrażenie i przesuwa je na wierzchu stosu.

binOp :: (Register -> Register -> Machine n n) -> Machine (S (S n)) (S n) 
compileExpr :: Expr -> Machine n (S n) 

Należy pamiętać, że jest to tylko proof-of-concept broić wokół rzeczą, mam tylko wysłał go do GitHub właśnie teraz pokazać, więc nie należy się spodziewać, aby znaleźć w niej coś wielkiego.

Answer 4

Prosty i wygodny? Nie jestem pewien.

Zacznę od opisu problemu. Zadanie polega na przejściu z nieformalnego do specyfikacji bliżej tego, co mamy w Haskell (typy).

Są tu dwa problemy: wymuszanie niezmienników opartych na typie w języku wejściowym (wyrażenia arytmetyczne?) I upewnianie się, że wyrażenie języka źródłowego skompilowane do programu stosu maszyn faktycznie wykonuje to, co chcemy.

Pierwsza z nich może być łatwo rozwiązana za pomocą GADT: wystarczy tylko wyliczyć wyrażenia według ich typów (np. Expr a dotyczy wyrażeń, które oceniają wartość typu a).

Po drugie, nie jestem tego pewien. Można oczywiście indeksować listy według naturałów na poziomie typu (na przykład przy użyciu GADT). Rodzaje niektórych funkcji na listach (takich jak głowa i ogon) stają się na tyle precyzyjne, że możemy je uczynić całkowitymi. Czy stos twojej maszyny do układania jest jednolity (to znaczy zawiera tylko liczby całkowite lub tylko duble lub ...)?

Inne właściwości mogą być również zakodowane (i wymuszane), ale przejście tej trasy może wymagać znacznego wysiłku ze strony programisty.