haskell - そのような制約が成立する場合、制約のないGADTを制約のある別のGADTに変換します

Question

コンストラクターに特定の制約のない GADT を、その制約を持つ GADT に変換できますか? 私がこれをしたいのは、矢印の深い埋め込みを取得し、(今のところ) が必要と思われる表現でいくつかの興味深いことをしたいからですTypeable。(理由は一つ)

data DSL a b where
  Id   :: DSL a a
  Comp :: DSL b c -> DSL a b -> DSL a c
  -- Other constructors for Arrow(Loop,Apply,etc)

data DSL2 a b where
  Id2   :: (Typeable a, Typeable b)             => DSL2 a a
  Comp2 :: (Typeable a, Typeable b, Typeable c) => DSL2 b c -> DSL2 a b -> DSL2 a c
  -- ...

次の関数を試すこともできますが、再帰ポイントfromの情報がないため、すぐに機能しなくなります。 Typeable

from :: (Typeable a, Typeable b) =>  DSL a b -> DSL2 a b
from (Id)       = Id2
from (Comp g f) = Comp2 (from g) (from f)

代わりに、型クラスで変換をキャプチャしようとします。しかし、それは破綻するだけでなく、実存的なTypeable b情報を失うことにもなります。b

class From a b where
  from :: a -> b

instance (Typeable a, Typeable b) => From (DSL a b) (DSL2 a b) where
  from (Id)       = Id2
  from (Comp g f) = Comp2 (from g) (from f)

他の提案はありますか？最終的には、型パラメーターに関する情報CategoryとArrow一緒に深い埋め込みを作成したいと考えています。Typeableこれは、アロー構文を使用して DSL で値を構築し、かなり標準的な Haskell コードを持つことができるようにするためです。多分私は Template Haskell に頼らなければなりませんか?

Answer 1

再帰ケースの問題は、 への変換にとって致命的DSL a bですDSL2 a b。

この変換を行うには、その場合Typeableの存在型の辞書を見つける必要がありますが、実際に何があるかはすでに忘れられています。bCompb

たとえば、次のプログラムを考えてみましょう。

data X = X Int
-- No Typeable instance for X

dsl1 :: DSL X Char
dsl1 = -- DSL needs to have some way to make non-identity terms,
       -- use whatever mechanism it offers for this.

dsl2 :: DSL Int X
dsl2 = -- DSL needs to have some way to make non-identity terms,
       -- use whatever mechanism it offers for this.

v :: DSL Int Char
v = Comp dsl1 dsl2

v2 :: DSL2 Int Char
v2 = -- made by converting v from DSL to DSL2, note that Int and Char are Typeable

typeOfIntermediate :: DSL a c -> TypeRep
typeOfIntermediate int =
    case int of
        Comp (bc :: DSL2 b c) (ab :: DSL2 a b) ->
            typeOf (undefined :: b)

typeOfX = typeOfIntermediate v2

言い換えれば、一般的に変換を行う方法があれば、Typeable実際にはインスタンスを持たない型のインスタンスをどうにか発明することができます。

Answer 2