#先日開催された第一回『プログラミング言語の基礎概念』の読書会ですこしだけ披露した導出システムを
##に置きました。
#今これの型レベル版
#に挑んでいるのですが，証明の印字するところでハマっています。
#質問の意図がぼくには伝わらなかったのですが、どのように pretty print すればいいのかということですか？
#証明をShowのインスタンスにしようとしているのですが，たとえば，
#data Times (n1 :: Nat) (n2 :: Nat) (n3 :: Nat) where
TZero :: Nat' n -> Times Z n Z
TSucc :: Nat' n1 -> Nat' n2 -> Nat' n3 -> Nat' n4
-> Times n1 n2 n3 -> Plus n2 n3 n4
-> Times (S n1) n2 n4#という定義をしておいて，
#instance Show (Nat' n) => Show (Plus Z n n) where
show (PZero n) = unwords [show Z',"plus",show n,"is",show n,"by","P-Zero","{","}"]
instance (Show (Nat' n1), Show (Nat' n2), Show (Nat' n3), Show (Plus n1 n2 n3))
=> Show (Plus (S n1) n2 (S n3)) where
show (PSucc n1 n2 n3 j1)
= unwords [show (S' n1),"plus",show n2,"is",show (S' n3),"by","P-Succ"
,"{",show j1,"}"]#のようにインスタンス宣言をしようとすると，1つめのインスタンス宣言は問題ないのですが，2つめは
#答を聞かずに脊髄反射しますが Show しないで pretty https://hackage.haskell.org/package/pretty とか使うのはどうですか #型レベルだと面倒なのかな
#j1がShowのインスタンスであることを導出できないという旨のエラーになります。
#type-level は関係なさそうで、Show の導出をどうするかという問題と理解したけどどうなのかな
#Text.Show.Functions が助けになればよいのですが
#はいそうです。凝った整形出力をするわけではないので，showが定義できれば十分なんです。
#<function>とでるだけだからならないな、すみません
#頻出する問題なのでぼくも解決法を知りたい
#あっ。コードを貼りまちがえた。Plusの方は問題ないんです。
#うまくいかないのは
#ghcの吐くエラーを出してもらえませんか
#instance (Show (Nat' n))
=> Show (Times Z n Z) where
show (TZero n) = unwords [show Z',"times", show n,"is",show Z',"by","{","}"]
instance (Show (Nat' n1),Show (Nat' n2),Show (Nat' n3) ,Show (Nat' n4)
,Show (Times n1 n2 n3), Show (Plus n2 n3 n4))
=> Show (Times (S n1) n2 n4) where
show (TSucc n1 n2 n3 n4 j1 j2)
= unwords [show (S' n1),"times",show n2,"is",show n4,"by","T-Succ","{"
,show j1,";",show j2
,"}"
]#こちらの2つめです。
#エラーは
#/home/nobsun/proj/hs-bcopl/src/Language/BCoPL/Nat.hs:49:16-19: Could not deduce (Show (Times n5 n2 n6)) …
arising from a use of ‘show’
from the context (Show (Nat' n1),
Show (Nat' n2),
Show (Nat' n3),
Show (Nat' n4),
Show (Times n1 n2 n3),
Show (Plus n2 n3 n4))
bound by the instance declaration
at /home/nobsun/proj/hs-bcopl/src/Language/BCoPL/Nat.hs:(44,10)-(46,35)
or from ('S n1 ~ 'S n5)
bound by a pattern with constructor
TSucc :: forall (n2 :: Nat) (n4 :: Nat) (n1 :: Nat) (n3 :: Nat).
Nat' n1
-> Nat' n2
-> Nat' n3
-> Nat' n4
-> Times n1 n2 n3
-> Plus n2 n3 n4
-> Times ('S n1) n2 n4,
in an equation for ‘show’
at /home/nobsun/proj/hs-bcopl/src/Language/BCoPL/Nat.hs:47:9-31
In the expression: show j1
In the first argument of ‘unwords’, namely
‘[show (S' n1), "times", show n2, "is", ....]’
In the expression:
unwords [show (S' n1), "times", show n2, "is", ....]
/home/nobsun/proj/hs-bcopl/src/Language/BCoPL/Nat.hs:49:28-31: Could not deduce (Show (Plus n2 n6 n4)) …
arising from a use of ‘show’
from the context (Show (Nat' n1),
Show (Nat' n2),
Show (Nat' n3),
Show (Nat' n4),
Show (Times n1 n2 n3),
Show (Plus n2 n3 n4))
bound by the instance declaration
at /home/nobsun/proj/hs-bcopl/src/Language/BCoPL/Nat.hs:(44,10)-(46,35)
or from ('S n1 ~ 'S n5)
bound by a pattern with constructor
TSucc :: forall (n2 :: Nat) (n4 :: Nat) (n1 :: Nat) (n3 :: Nat).
Nat' n1
-> Nat' n2
-> Nat' n3
-> Na#ぐぐってみたらGADTでそういう問題は起こるんやというものをいくつか見ました、ボクはまだその理由を把握してない
#Times は3つの自然数型を引数としてとるのですが，その構成子の1つであるTSuccが4つめの自然数型を必要としていて，そいつに関しての制約が解消できないからだと思うんですが，なにかこれを解消するHackがないかなぁと。。。
#近づいたので再掲。7月16日（木）「平日夜にすごいH本をちょびちょび読む会 16回目」（定員4名） #Hちょびよみ http://hchobi.connpass.com/event/17616/ この読書会のモットーの「いのちをだいじにしながら」「人が死なない」というのが好き。 
haskell-ja > Archives > 2015/07/15