Wymyśliłem rozwiązanie, które wykorzystuje system typu Haskell. Poszukałem trochę istniejącego rozwiązania problemu na poziomie wartości , nieco go zmieniłem, a następnie podniosłem do poziomu typu. Wymyśliłem wiele na nowo. Musiałem także włączyć kilka rozszerzeń GHC.
Po pierwsze, ponieważ liczby całkowite nie są dozwolone na poziomie typu, musiałem ponownie odkryć liczby naturalne, tym razem jako typy:
data Zero -- type that represents zero
data S n -- type constructor that constructs the successor of another natural number
-- Some numbers shortcuts
type One = S Zero
type Two = S One
type Three = S Two
type Four = S Three
type Five = S Four
type Six = S Five
type Seven = S Six
type Eight = S Seven
Algorytm, który zaadaptowałem, dodaje i odejmuje wartości naturalne, więc musiałem je też wymyślić na nowo. Funkcje na poziomie typu są definiowane za pomocą klas typów. Wymaga to rozszerzenia wielu klas typów parametrów i zależności funkcjonalnych. Klasy typów nie mogą „zwracać wartości”, dlatego używamy do tego dodatkowego parametru, w sposób podobny do PROLOG.
class Add a b r | a b -> r -- last param is the result
instance Add Zero b b -- 0 + b = b
instance (Add a b r) => Add (S a) b (S r) -- S(a) + b = S(a + b)
class Sub a b r | a b -> r
instance Sub a Zero a -- a - 0 = a
instance (Sub a b r) => Sub (S a) (S b) r -- S(a) - S(b) = a - b
Rekurencja jest implementowana z asercjami klas, więc składnia wygląda nieco wstecz.
Następne były booleany:
data True -- type that represents truth
data False -- type that represents falsehood
I funkcja do porównywania nierówności:
class NotEq a b r | a b -> r
instance NotEq Zero Zero False -- 0 /= 0 = False
instance NotEq (S a) Zero True -- S(a) /= 0 = True
instance NotEq Zero (S a) True -- 0 /= S(a) = True
instance (NotEq a b r) => NotEq (S a) (S b) r -- S(a) /= S(b) = a /= b
I listy ...
data Nil
data h ::: t
infixr 0 :::
class Append xs ys r | xs ys -> r
instance Append Nil ys ys -- [] ++ _ = []
instance (Append xs ys rec) => Append (x ::: xs) ys (x ::: rec) -- (x:xs) ++ ys = x:(xs ++ ys)
class Concat xs r | xs -> r
instance Concat Nil Nil -- concat [] = []
instance (Concat xs rec, Append x rec r) => Concat (x ::: xs) r -- concat (x:xs) = x ++ concat xs
class And l r | l -> r
instance And Nil True -- and [] = True
instance And (False ::: t) False -- and (False:_) = False
instance (And t r) => And (True ::: t) r -- and (True:t) = and t
ifbrakuje również na poziomie typu ...
class Cond c t e r | c t e -> r
instance Cond True t e t -- cond True t _ = t
instance Cond False t e e -- cond False _ e = e
Dzięki temu wszystkie maszyny pomocnicze, których użyłem, były na miejscu. Czas rozwiązać sam problem!
Rozpoczęcie od funkcji sprawdzania, czy dodanie królowej do istniejącej planszy jest w porządku:
-- Testing if it's safe to add a queen
class Safe x b n r | x b n -> r
instance Safe x Nil n True -- safe x [] n = True
instance (Safe x y (S n) rec,
Add c n cpn, Sub c n cmn,
NotEq x c c1, NotEq x cpn c2, NotEq x cmn c3,
And (c1 ::: c2 ::: c3 ::: rec ::: Nil) r) => Safe x (c ::: y) n r
-- safe x (c:y) n = and [ x /= c , x /= c + n , x /= c - n , safe x y (n+1)]
Zwróć uwagę na użycie asercji klasowych w celu uzyskania wyników pośrednich. Ponieważ zwracane wartości są w rzeczywistości dodatkowym parametrem, nie możemy po prostu wywoływać asercji bezpośrednio od siebie. Ponownie, jeśli używałeś PROLOGA, możesz uznać ten styl za nieco znajomy.
Po wprowadzeniu kilku zmian w celu wyeliminowania potrzeby używania lambda (które mogłem wdrożyć, ale postanowiłem wyjechać na kolejny dzień), tak wyglądało oryginalne rozwiązanie:
queens 0 = [[]]
-- The original used the list monad. I "unrolled" bind into concat & map.
queens n = concat $ map f $ queens (n-1)
g y x = if safe x y 1 then [x:y] else []
f y = concat $ map (g y) [1..8]
mapjest funkcją wyższego rzędu. Myślałem, że zaimplementowanie meta-funkcji wyższego rzędu byłoby zbyt dużym problemem (znowu lambdas), więc po prostu wybrałem prostsze rozwiązanie: ponieważ wiem, które funkcje będą mapowane, mogę zaimplementować mapdla nich specjalizowane wersje , aby nie były funkcje wyższego rzędu.
-- Auxiliary meta-functions
class G y x r | y x -> r
instance (Safe x y One s, Cond s ((x ::: y) ::: Nil) Nil r) => G y x r
class MapG y l r | y l -> r
instance MapG y Nil Nil
instance (MapG y xs rec, G y x g) => MapG y (x ::: xs) (g ::: rec)
-- Shortcut for [1..8]
type OneToEight = One ::: Two ::: Three ::: Four ::: Five ::: Six ::: Seven ::: Eight ::: Nil
class F y r | y -> r
instance (MapG y OneToEight m, Concat m r) => F y r -- f y = concat $ map (g y) [1..8]
class MapF l r | l -> r
instance MapF Nil Nil
instance (MapF xs rec, F x f) => MapF (x ::: xs) (f ::: rec)
A ostatnią meta-funkcję można teraz napisać:
class Queens n r | n -> r
instance Queens Zero (Nil ::: Nil)
instance (Queens n rec, MapF rec m, Concat m r) => Queens (S n) r
Pozostało po prostu jakiś sterownik, który nakłonił maszynę do sprawdzania typu do wypracowania rozwiązań.
-- dummy value of type Eight
eight = undefined :: Eight
-- dummy function that asserts the Queens class
queens :: Queens n r => n -> r
queens = const undefined
Ten metaprogram ma działać na narzędziu sprawdzania typu, więc można odpalić ghcii zapytać o typ queens eight:
> :t queens eight
To dość szybko przekroczy domyślny limit rekurencji (to marne 20). Aby zwiększyć ten limit, musimy wywołać ghciz -fcontext-stack=Nopcją, gdzie Njest pożądana głębokość stosu (N = 1000 i piętnaście minut to za mało). Nie widziałem jeszcze tego ukończenia, ponieważ zajmuje to bardzo dużo czasu, ale udało mi się do niego dotrzeć queens four.
Jest idealny program na ideone z niektórymi maszynami do ładnego drukowania typów wyników, ale queens twomoże działać tylko bez przekraczania limitów :(