Haskellのインスタンスタイプ変数
-
12-10-2019 - |
質問
編集:解決しました。 私は、ソースファイルで言語拡張機能を有効にしても、GHCIの言語拡張機能を有効にしていないことを認めていました。解決策は次のとおりでした :set FlexibleContexts
GHCIで。
私は最近、クラスのタイプ宣言とHaskellのインスタンスがホーン条項であることを発見しました。そこで、算術操作をエンコードしました プロログの芸術, 、第3章、Haskellへ。例えば:
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
Prologでは、証明に値が(ロジック)変数に対してインスタンス化されます。ただし、Haskellのタイプ変数をインスタンス化する方法がわかりません。つまり、プロログクエリに相当するHaskellが何であるかわかりません
?-f(X1,X2,...,Xn)
は。私はそれを想定しています
:t undefined :: (f x1 x2 ... xn) => xi
Haskellがインスタンス化されます xi
, 、しかし、これはを与えます Non type-variable argument in the constraint
でもエラー FlexibleContexts
有効になっています。
解決
プロログサンプルについてはわかりませんが、これを次のように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が次のように彼のコメントで指摘したように、「Lazy Pattern」(例えば、文脈で)はここでは必要ありません(彼の最初のコードは短く、よりクリーンです)。
このパターンの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
しかし、これは「機能的依存関係の競合」のためにコンパイルされません。そして、私たちはまだ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
それは間違いなく最も素晴らしい方法ではありません(それはインコヘンティンステンスを必要とします)。だから、誰かが別の、それほど「トラウマ的」なアプローチを提案できるかもしれません。