私は、いくつかの適切な形式の側面の制約を保証し、その中でミューバインディングを展開できるようにする、おもちゃの通常の型システムを実装しようとしています。これらの型を表すデータ型には、固定小数点のコンストラクター ( Mu)、最も近い Mu 境界項による置換 ( Var)、ゼロおよび 1 つの引数型演算子 (それぞれNullaryおよびUnary) が含まれます。
これらの型が適切な形式であることを確認するために、ヘッド コンストラクターとして a を持っているか、ヘッド コンストラクターとしてa を持っているか、またはその中のどこかに aBoolがあるかを、3 つのパラメーターとして追跡します。MuVarVar
data A : Bool -- Is Mu headed?
-> Bool -- Is Var headed?
-> Bool -- Contains any Var's?
-> Type where
Mu : A False False _ -> A True False False
Var : A False True True
Nullary : A False False False
Unary : A _ _ m -> A False False m
Mu ヘッド型の展開を実装するには、置換を実行する必要があります。具体的には、「Mu x. F ====> F[(Mu x. F)/x]」を実装する必要があります。
3 番目の型パラメーターが機能することの証明を生成する必要があることを除けば、この関数substは簡単に見えます。
total subst : A m1 v1 c1 -> A m2 v2 c2 -> (c3 ** ((A (m2 || (v2 && m1))
(v2 && v1)
c3)
,(c3 = (c2 && c1))))
subst _ Nullary = (_ ** (Nullary,Refl))
subst w (Unary a) with (subst w a)
| (c3** (a',aeq)) = (c3 ** (Unary a',aeq))
subst w Var = (_ ** (w,Refl))
subst w (Mu a) = (_ ** (Mu a,Refl))
この戻り値の型を少しクリーンアップするラッパーを作成しようとしましたが、失敗しました。
total subst' : A m1 v1 c1 -> A m2 v2 c2 -> A (m2 || (v2 && m1))
(v2 && v1)
(c2 && c1)
subst' a1 a2 with (subst a2 a2)
| (_**(a',aeq)) ?= a'
このメタ変数を解こうとすると、期待どおりでaeq : x = c2 && Delay c2はないことがわかりましaeq : x = c2 && Delay c1た (( &&) が 2 番目の引数で遅延していることを思い出してください)。
私は何か間違ったことをしていますか？これは予想される動作ですか？FWIW、展開用の非常によく似たラッパーを正常に作成しました（表示されていません）。