Haskellで型変数をインスタンス化する

Question

EDIT：解決済み。ソースファイルで言語拡張を有効にしてもGHCiで言語拡張が有効になっていないことはわかりませんでした。解はGHCiにおいて:set FlexibleContextsであった。

---

私は最近、Haskellのクラスとインスタンスの型宣言がホーン節であることを発見しました。そこで、私は、のプロローグのテクニックの第3章をハスケルに符号化しました。例えば：Prologで

fac(0,s(0)). 
fac(s(N),F) :- fac(N,X), mult(s(N),X,F). 

class Fac x y | x -> y 
instance Fac Z (S Z) 
instance (Fac n x, Mult (S n) x f) => Fac (S n) f 

pow(s(X),0,0) :- nat(X). 
pow(0,s(X),s(0)) :- nat(X). 
pow(s(N),X,Y) :- pow(N,X,Z), mult(Z,X,Y). 

class Pow x y z | x y -> z 
instance (N n) => Pow (S n) Z Z 
instance (N n) => Pow Z (S n) (S Z) 
instance (Pow n x z, Mult z x y) => Pow (S n) x y 

、値はプルーフで（ロジック）の変数のためにインスタンス化されます。しかし、私はHaskellで型変数をインスタンス化する方法を理解していません。つまり、私はPrologクエリのハスケル相当のものを理解していません。

?-f(X1,X2,...,Xn) 

です。私はFlexibleContextsが有効になっていても、

:t undefined :: (f x1 x2 ... xn) => xi 

は、Haskellはxiをインスタンス化する原因となるが、これはNon type-variable argument in the constraintエラーを与えることを前提としています。

Answer 1

Prologのサンプルについての確認が、私は次のようにHaskellでこれを定義します

{-# LANGUAGE MultiParamTypeClasses, EmptyDataDecls, FlexibleInstances, 
FlexibleContexts, UndecidableInstances, TypeFamilies, ScopedTypeVariables #-} 

data Z 
data S a 
type One = S Z 
type Two = S One 
type Three = S Two 
type Four = S Three 


class Plus x y r 
instance (r ~ a) => Plus Z a r 
instance (Plus a b p, r ~ S p) => Plus (S a) b r 

p1 = undefined :: (Plus Two Three r) => r 


class Mult x y r 
instance (r ~ Z) => Mult Z a r 
instance (Mult a b m, Plus m b r) => Mult (S a) b r 

m1 = undefined :: (Mult Two Four r) => r 


class Fac x r 
instance (r ~ One) => Fac Z r 
instance (Fac n r1, Mult (S n) r1 r) => Fac (S n) r 

f1 = undefined :: (Fac Three r) => r 


class Pow x y r 
instance (r ~ One) => Pow x Z r 
instance (r ~ Z) => Pow Z y r 
instance (Pow x y z, Mult z x r) => Pow x (S y) r 

pw1 = undefined :: (Pow Two Four r) => r 

-- Handy output 
class (Num n) => ToNum a n where 
    toNum :: a -> n 
instance (Num n) => ToNum Z n where 
    toNum _ = 0 
instance (ToNum a n) => ToNum (S a) n where 
    toNum _ = 1 + toNum (undefined :: a) 

main = print $ (toNum p1, toNum m1, toNum f1, toNum pw1) 

更新：danportinとして

がTypeFamilies "レイジーパターン" 下の彼のコメントで指摘（インスタンスコンテキストでは）ここでは必要ありません（彼の初期コードは短く、よりクリーンです）。

私はこの質問の文脈で考えることができますが、このパターンの1つの応用は、これです：

data HTrue 
data HFalse 

-- Will not compile 
class And x y r | x y -> r 
instance And HTrue HTrue HTrue 
instance And a b HFalse -- we do not what to enumerate all the combination here - they all HFalse 

しかし、これはしません：我々はタイプレベルの算術にブール論理を追加したいと"Functional dependencies conflict"のためにコンパイルしてください。 そしてそれは、我々はまだfundepsせずに、この重複ケースを表現できるように私には見えます：

class And x y r 
instance (r ~ HTrue) => And HTrue HTrue r 
instance (r ~ HFalse) => And a b r 

b1 = undefined :: And HTrue HTrue r => r -- HTrue 
b2 = undefined :: And HTrue HFalse r => r -- HFalse 

それは間違いなく（それはIncoherentInstancesが必要です）素敵な方法ではありません。だから、誰かが別の、より少ない「トラウマ的な」アプローチを提案するかもしれない。