simple type level predicates in haskell

Prolog.hs

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
module Prolog (Petja, Vasja, Serg, Father) where 

data Petja = Petja
data Vasja = Vasja
data Serg = Serg

class Father a b where
	isFather :: a -> b -> ()
	isFather x y = ()
	  

instance Father Vasja Petja
instance Father Petja Serg

class Son a b where
	isSon :: a -> b -> ()
	isSon x y = ()


instance (Father b a) => Son a b

class GrandFather a b c where
	isGrandFather :: a -> c -> ()
	isGrandFather x y = ()

instance (Father a b, Father b c) => GrandFather a b c

Прикольно. Так а что насчёт судоку? (;

Не получится. Даже эти примеры работают только с ограничениями. Кстати первая версия была с ошибкой и эта тоже. Например Дедуля работать не будет. Может быть это возможно обойти но в любом случае очень тяжело написать полностью непротиворечивую систему. А насчет судоку я все таки попробую если будет время.

А зачем GrandFather нужен b?

А как иначе ты найдешь? X является дедушкой Y в том случае если X является отцом кого либо кто в свою очередь является отцом Y. Как раз пролог в таких случаях перебирает все возможные варианты и подставляет в b. В моем примере этого не происходит я еще не разобрался почему. Если знаешь другой способ подскажи.

хм, я не разбираюсь вообще-то в этом, но где-то краем уха слышал про Functional Depencies. Ну вот если их тут применить, то всё заработает. Необходимых изменений минимум:

{-# LANGUAGE FunctionalDependencies #-}

...

class Father a b | b -> a where
    ...

...

class GrandFather a c where
    ...

instance (Father a b, Father b c) => GrandFather a c

Слова Father a b | b -> a означают, что по сути, что у сына только один отец – родителей не выбирают (; То есть по типу сына b тип отца a определяется однозначно. Логично ввести такие же ограничения и у классов Son и GrandFather.

сенкс

Хм а получается что у отца может быть только один сын?

Интересно надо будет поэкспериментировать.

Вроде как нет. Я создавал нескольких детей и всё было ок. Даже сделал класс Brothers ")