バウンドを使用した相互再帰構文

Question

次は、依存型のラムダ計算の構文です。

data TermI a = Var a 
      | App (TermI a) (TermC a) -- when type-checking an application, infer the type of the function and then check that its argument matches the domain 
      | Star -- the type of types 
      | Pi (Type a) (Scope() Type a) -- The range of a pi-type is allowed to refer to the argument's value 
      | Ann (TermC a) (Type a) -- embed a checkable term by declaring its type 
      deriving (Functor, Foldable, Traversable) 

data TermC a = Inf (TermI a) -- embed an inferrable term 
      | Lam (Scope() TermC a) 
      deriving (Functor, Foldable, Traversable) 

type Type = TermC -- types are values in a dependent type system 

（Iは多かれ少なかれSimply Easyからこれを持ち上げ。）型システムは、その型タイピングコンテキストから推測することができるものに用語を分割、bidirectionalであり、そして唯一の目標に照らしてチェックすることができるものタイプ。従属型システムでは、一般にラムダ項にはプリンシパル型がないため、これは便利です。

とにかく、私はこの構文のためMonadインスタンスを定義しようとして捕まってしまったしました：

instance Monad TermI where 
    return = Var 
    Var x >>= f = f x 
    App fun arg >>= f = App (fun >>= f) (arg >>= Inf . f) -- embed the substituted TermI into TermC using Inf 
    Star >>= _ = Star 
    Pi domain range >>= f = Pi (domain >>= Inf . f) (range >>>= Inf . f) 
    Ann term ty >>= f = Ann (term >>= Inf . f) (ty >>= Inf . f) 

instance Monad TermC where 
    return = Inf . return 
    Lam body >>= f = Lam (body >>>= f) 
    Inf term >>= f = Inf (term >>= _) 

をTermCのインスタンスの最後の行の穴を埋めるために、私はタイプa -> TermI bの何かを必要とするが、fタイプはa -> TermC bです。 TermCの型がわからないので、結果としてTermCをTermIに埋め込むことはできません。Annコンストラクタを使用します。

このデータ型はboundのモデルと互換性がありませんか？または、Monadインスタンスを作成するために使用できるトリックがありますか？

Answer 1

これは非常に単純に不可能です。TermCはモナドではありません。置換は変数の代わりに用語を置きます。これが意味を成すためには、用語は適合することができなければならない。すなわち、得られる用語が依然として良好な特性を有するように十分に類似である必要がある。ここでは、そのタイプが推測可能でなければならないことを意味します。 TermCはしません。

あなたは、実装することができ、次のいずれか[\ X - > X]

substI :: TermI a -> (a -> TermI b) -> TermI b 
substC :: TermC a -> (a -> TermI b) -> TermC b 

を、あなたは（表記を乱用） `（VAR 0（VAR 1））を実行した場合

instance Monad TermI where 
    return = Var 
    bind = substI