うまくいけば、より多くの経験を持つ誰かが、より洗練された、戦いでテストされた、すぐに使える答えを持っているでしょうが、これが私のショットです。
GADTを使用すると、比較的少ないコストでパイを持ってその一部を食べることができます。
{-# LANGUAGE GADTs #-}
data P0 -- phase zero
data P1 -- phase one
data Type p where
TypeInt :: Id -> Type p
TypePointer :: Id -> Type p -> Type p -- target type
TypeArray :: Id -> Type p -> Expr p -> Type p -- elt type, elt count
TypeStruct :: Id -> [(String, Type p)] -> Type p -- [(field name, field type)]
TypeOf :: Id -> Expr P0 -> Type P0
TypeDef :: Id -> Type P0 -> Type P0
data Expr p where
ExprInt :: Int -> Expr p -- literal int
ExprVar :: Var -> Expr p -- variable
ExprSizeof :: Type P0 -> Expr P0
ExprUnop :: Unop -> Expr p -> Expr p
ExprBinop :: Binop -> Expr p -> Expr p -> Expr p
ExprField :: Bool -> Expr P0 -> String -> Expr P0 -- Bool gives true=>s.field, false=>p->field
ここで変更したものは次のとおりです。
データ型はGADT構文を使用するようになりました。これは、コンストラクターが型アノテーションを使用して宣言されることを意味します。data Foo = Bar Int Char
になりdata Foo where Bar :: Int -> Char -> Foo
ます(構文を除けば、2つは完全に同等です)。
との両方に型変数を追加しましType
たExpr
。これは、いわゆるファントム型変数です。型の実際のデータは格納されてp
おらず、型システムで不変条件を適用するためにのみ使用されます。
変換の前後のフェーズを表すダミータイプを宣言しました:フェーズ0とフェーズ1。(複数のフェーズを持つより複雑なシステムでは、タイプレベルの番号を使用してそれらを示すことができる可能性があります。)
GADTを使用すると、タイプレベルの不変条件をデータ構造に格納できます。ここに2つあります。1つ目は、再帰的な位置は、それらを含む構造と同じフェーズでなければならないということです。たとえば、を見ると、コンストラクターにTypePointer :: Id -> Type p -> Type p
aを渡して、結果としてaを取得します。これらのは、同じ型である必要があります。(異なるタイプを許可したい場合は、とを使用できます。)Type p
TypePointer
Type p
p
p
q
2つ目は、一部のコンストラクターは最初のフェーズでのみ使用できるという事実を強制することです。ほとんどのコンストラクターはファントム型変数p
でポリモーフィックですが、一部のコンストラクターではそれがである必要がありますP0
。つまり、これらのコンストラクターは、タイプType P0
またはの値を作成するためにのみ使用できExpr P0
、他のフェーズは使用できません。
GADTは2つの方向で機能します。1つ目は、を返す関数がありType P1
、それを構築するためにを返すコンストラクターの1つを使用しようとするとType P0
、型エラーが発生することです。これは「構築による修正」と呼ばれるものです。無効な構造を構築することは静的に不可能です(型システムで関連するすべての不変条件をエンコードできる場合)。逆に、の値がある場合はType P1
、正しく構築されていることを確認できます。コンストラクターTypeOf
とTypeDef
コンストラクターは使用できません(実際、それらでパターンマッチングを行おうとすると、コンパイラーは文句を言います) 、および再帰的な位置もフェーズである必要がありますP1
。基本的に、GADTを作成するときは、型の制約が満たされているという証拠を保存し、パターンマッチを行うときは、その証拠を取得して利用できます。
それは簡単な部分でした。残念ながら、2つのタイプの間には、コンストラクターが許可される範囲を超えていくつかの違いがあります。コンストラクター引数の一部はフェーズ間で異なり、一部は変換後のフェーズにのみ存在します。GADTを使用してこれをエンコードすることもできますが、低コストでエレガントではありません。1つの解決策は、異なるコンストラクターをすべて複製し、とにそれぞれ1つずつ持つことP0
ですP1
。しかし、複製は良くありません。私たちはそれをよりきめ細かくすることを試みることができます:
-- a couple of helper types
-- here I take advantage of the fact that of the things only present in one phase,
-- they're always present in P1 and not P0, and not vice versa
data MaybeP p a where
NothingP :: MaybeP P0 a
JustP :: a -> MaybeP P1 a
data EitherP p a b where
LeftP :: a -> EitherP P0 a b
RightP :: b -> EitherP P1 a b
data Type p where
TypeInt :: Id -> Type p
TypePointer :: Id -> Type p -> Type p
TypeArray :: Id -> Type p -> EitherP p (Expr p) Int -> Type p
TypeStruct :: Id -> [(String, MaybeP p Int, Type p)] -> Type p
TypeOf :: Id -> Expr P0 -> Type P0
TypeDef :: Id -> Type P0 -> Type P0
-- for brevity
type MaybeType p = MaybeP p (Type p)
data Expr p where
ExprInt :: MaybeType p -> Int -> Expr p
ExprVar :: MaybeType p -> Var -> Expr p
ExprSizeof :: Type P0 -> Expr P0
ExprUnop :: MaybeType p -> Unop -> Expr p -> Expr p
ExprBinop :: MaybeType p -> Binop -> Expr p -> Expr p -> Expr p
ExprField :: Bool -> Expr P0 -> String -> Expr P0
MaybeP
ここでは、いくつかのヘルパータイプを使用して、一部のコンストラクター引数はフェーズ1( )にのみ存在でき、一部は2つのフェーズ()間で異なるという事実を強制しましたEitherP
。これにより完全にタイプセーフになりますが、少しアドホックな感じがします。それでも、常にMaybeP
sとEitherP
sの内外で物事をラップする必要があります。その点でもっと良い解決策があるかどうかはわかりません。ただし、完全な型安全性は何かですfromJustP :: MaybeP P1 a -> a
。完全かつ完全に安全であることを記述して確認することができます。
更新:別の方法は次を使用することTypeFamilies
です:
data Proxy a = Proxy
class Phase p where
type MaybeP p a
type EitherP p a b
maybeP :: Proxy p -> MaybeP p a -> Maybe a
eitherP :: Proxy p -> EitherP p a b -> Either a b
phase :: Proxy p
phase = Proxy
instance Phase P0 where
type MaybeP P0 a = ()
type EitherP P0 a b = a
maybeP _ _ = Nothing
eitherP _ a = Left a
instance Phase P1 where
type MaybeP P1 a = a
type EitherP P1 a b = b
maybeP _ a = Just a
eitherP _ a = Right a
Expr
以前のバージョンとの唯一の変更点Type
は、コンストラクターにPhase p
制約を追加する必要があることExprInt :: Phase p => MaybeType p -> Int -> Expr p
です。
ここp
で、Type
またはのタイプがわかっている場合は、 sがであるか、指定されたタイプであるか、およびsがどのタイプであるExpr
かを静的に知ることができ、明示的にアンラップすることなく、それらをそのタイプとして直接使用できます。不明な場合は、クラスから使用して、それらが何であるかを調べることができます。(引数が必要です。そうしないと、コンパイラーは意図したフェーズを判断できません。)これはGADTバージョンに類似しており、既知の場合は何が含まれているのかを確認できますが、そうでない場合は次のようになります。両方の可能性にパターンマッチします。この解決策は、「欠落している」引数が次のようになるという点でも完全ではありません。MaybeP
()
EitherP
p
maybeP
eitherP
Phase
Proxy
p
MaybeP
EitherP
()
完全に消えるのではなく。
sExpr
とType
sの作成も、2つのバージョン間でほぼ同じように見えます。作成する値にフェーズ固有の値がある場合は、そのタイプでそのフェーズを指定する必要があります。p
多態的な関数を記述したいが、それでもフェーズ固有の部分を処理したい場合に問題が発生するようです。GADTを使用すると、これは簡単です。
asdf :: MaybeP p a -> MaybeP p a
asdf NothingP = NothingP
asdf (JustP a) = JustP a
asdf _ = NothingP
出力のタイプが入力と同じであることが保証されないため、私が単に記述した場合、コンパイラは文句を言うことに注意してください。パターンマッチングにより、入力がどのタイプであるかを把握し、同じタイプの結果を返すことができます。
ただし、このTypeFamilies
バージョンでは、これは非常に困難です。使用するだけmaybeP
で、結果としてMaybe
、型についてコンパイラに何も証明できません。maybeP
を持ってeitherP
戻る代わりに、Maybe
とのようにEither
デコンストラクター関数を作成することで、その途中の一部を取得できます。これにより、型の同等性も利用できるようになります。maybe
either
maybeP :: Proxy p -> (p ~ P0 => r) -> (p ~ P1 => a -> r) -> MaybeP p a -> r
eitherP :: Proxy p -> (p ~ P0 => a -> r) -> (p ~ P1 => b -> r) -> EitherP p a b -> r
(これが必要であることに注意してください。また、これらは基本的にとRank2Types
のGADTバージョンのCPS変換バージョンであることに注意してください。)MaybeP
EitherP
次に、次のように書くことができます。
asdf :: Phase p => MaybeP p a -> MaybeP p a
asdf a = maybeP phase () id a
しかし、GHCは次のように述べているため、それでも十分ではありません。
data.hs:116:29:
Could not deduce (MaybeP p a ~ MaybeP p0 a0)
from the context (Phase p)
bound by the type signature for
asdf :: Phase p => MaybeP p a -> MaybeP p a
at data.hs:116:1-29
NB: `MaybeP' is a type function, and may not be injective
In the fourth argument of `maybeP', namely `a'
In the expression: maybeP phase () id a
In an equation for `asdf': asdf a = maybeP phase () id a
どこかで型アノテーションを使ってこれを解決できるかもしれませんが、その時点では、それは価値があるよりも面倒なようです。したがって、他の誰かからのさらなる情報が保留されているので、少し構文上のノイズを犠牲にして、より単純でより堅牢なGADTバージョンを使用することをお勧めします。
再度更新する:ここでの問題MaybeP p a
は、は型関数であり、他に通過する情報がないため、GHCには何p
をa
すべきかを知る方法がないということでした。を渡して、Proxy p
その代わりにそれを使用すると、がphase
解決されますが、それでも不明です。p
a