1

私はHaskellの科目について、次のことを与えられた大学からの継続演習を行っています。

data Expr = Con Value
          | And Expr Expr

data Value = IntValue  Int
           | BoolValue Bool

est :: Expr -> Val
est (Con v) = v
est (And x y) = 
  case (est x, est y) of
    (BoolValue bool1, BoolValue bool2) -> BoolValue $ bool1 && bool2
    _                    -> error "And: expected Boolean arguments"

そして、それが本当に何をするのかわかりません。で定義されている用語の評価者のようExprです。誰かが私にそれを説明してもらえますか？私の演習では、それを次のように実行したGADTに変換します。

data Expr e where
  Con :: Val -> Expr Val
  And :: Expr e -> Expr e -> Expr e

今、彼らは私に以下を静的に実装し、それをタイプセーフにするように求めています：

est :: Expr e -> e
est _ = -- implement this
4

2 に答える 2

4

GADTの方向性が間違っていると思います。その理由を理解するために、最初にの型なしバージョンExprとその評価者（質問の最初の部分）を見ていきます。

Expr作成できるタイプの値は次のとおりです。

expr1 = Con (IntValue 42)
expr2 = Con (BoolValue True)
expr3 = Con (BoolValue False)

これまでのところ、とても良いです：expr1整数定数42、expr2およびexpr3ブール定数Trueとを表しFalseます。Expr最も外側のコンストラクターとしての型のすべての値は、Con基本的に次のようになります。

Andコンストラクターをミックスに追加すると、物事が面白くなり始めます。

expr4 = And (Con (BoolValue True)) (Con (BoolValue True))
expr5 = And (Con (BoolValue True)) (And (Con (BoolValue False)) (Con (BoolValue False)))
expr6 = And (Con (BoolValue True)) (Con (IntValue 42))

expr4そしてexpr5大丈夫です。それらはそれぞれ式True && TrueとTrue && (False && False)を表します。True私たちは彼らがとに評価することを期待しますFalseが、それについてはすぐに詳しく説明します。しかし、expr6怪しげに見えます。それはTrue && 42意味をなさない表現を表しています（少なくともHaskellでは！）。

これまで見てきた式は、6番を除いて、すべて値があります。整数値は42で、expr1残りはブール値です（ s 2から5の場合は、、、）。ご覧のとおり、値は整数またはブール値のいずれかであるため、タイプの値として表すことができます。TrueFalseTrueFalseexprValue

Exprを取り、そのを返すエバリュエーターを書くことができますValue。つまり、エバリュエーターは定数式の値を返す必要があり、式が論理'および'の場合、ブール値である必要がある構成式の値の論理'および'を返す必要があります-できませんand整数とブール値、または2つの整数の論理積を取ります。コードでは、これは次のように変換されます

est :: Expr -> Value -- takes an Expr and returns its Value
est (Con value) = value -- the value of a constant expression is the wrapped value
est (And e1 e2) = let value1 = est e1 -- the value of the first operand
                      value2 = est e2 -- the value of the second operand
                  in logicalAndValue value1 value2

logicalAndValue :: Value -> Value -> Value
logicalAndValue (BoolValue b1) (BoolValue b2) = BoolValue (b1 && b2)
logicalAndValue (BoolValue b1) (IntValue i2)  = error "Can't take the logical 'and' of a boolean and an integer" 
logicalAndValue (IntValue i1)  (BoolValue b2) = error "Can't take the logical 'and' of an integer and a boolean"
logicalAndValue (IntValue i1)  (IntValue i2)  = error "Can't take the logical 'and' of two integers"

これは、最初ののより冗長なバージョンであり、est2つの評価された式の論理'および'を別の関数にスピンオフし、わずかに有益なエラーメッセージを表示する操作が含まれています。

さて、うまくいけば、これはあなたの最初の質問に答えます！問題は、Expr値がブール値または整数値のいずれかを持つ可能性があり、その型を「見る」ことができなくなるという事実に要約されます。したがって、Andこれが意味をなさない2つの式を一緒にすることができます。

これを解決する1つの方法は、Expr2つの新しい式タイプに分割することです。1つは整数値を持ち、もう1つはブール値を持ちます。これは次のようになります（expr上記で使用したのと同等のものも示します）。

data IntExpr = ConInt Int
expr1 :: IntExpr
expr1 = ConInt 42

data BoolExpr = ConBool Bool
              | AndBool BoolExpr BoolExpr
expr2 :: BoolExpr
expr2 = ConBool True
expr3 = ConBool False
expr4 = AndBool (ConBool True) (ConBool True)
expr5 = AndBool (ConBool True) (AndBool (ConBool False) (ConBool False))

注目すべき2つの点があります。Value型を削除しましたが、同等のものを作成することができexpr6なくなりました。これは、その明らかな変換AndBool (ConBool True) (ConInt 42)がコンパイラによって拒否されるためです（これを試す価値があるかもしれません）。型エラーの：ConInt 42型IntExprであり、それをの2番目の引数として使用することはできませんAndBool。

評価者には、整数式用とブール式用の2つのバージョンも必要です。それらを書きましょう！値がIntExpr必要であり、 sに評価される必要があります。IntBoolExprBool

 evalInt :: IntExpr -> Int
 evalInt (ConInt n) = n

 evalBool :: BoolExpr -> Bool
 evalBool (ConBool b) = b
 evalBool (AndBool e1 e2) = let v1 = evalBool e1 -- v1 is a Bool
                                v2 = evalBool e2 -- v2 as well
                            in v1 && v2

ご想像のとおり、これは、より多くのタイプの式（Char、lists、Doubleなど）を追加したり、2つの数値を追加したり、「if」式を作成したり、タイプが指定されていない変数を作成したりするなど、式を組み合わせる方法を追加すると、面倒になります。あらかじめ...

これがGADTの出番です！評価の可能な結果タイプ（IntExprおよびそれBoolExpr以上）ごとに個別のタイプの式を作成する代わりに、評価するタイプで式タイプ自体に「タグ付け」します。したがって、typeの値を評価した結果がであり、aが。を与えることを確認します。実際には、（上記の関数のように）実行時にタイプチェックを実行するのではなく、コンパイラにタイプチェックを実行させます。Expr IntIntExpr BoolBoollogicalAndValue

今のところ、式を作成する方法は2つだけです。定数式を作成する方法と、2つのブール値を一緒に'および'-する方法です。最初の方法は次のように機能します。があればInt、それをに変換し、をExpr IntにBool変換Expr Boolします。したがって、「makeconstantexpression」コンストラクターの型アノテーションは次のようになります。

Con :: v -> Expr v

2番目のコンストラクターはブール値を表す2つの式を取り（したがって、これらの2つの式はタイプですExpr Bool）、ブール値を持つ別の式を返します。つまり、このコンストラクターのタイプは次のとおりです。

And :: Expr Bool -> Expr Bool -> Expr Bool

ピースをまとめると、次のExprタイプが得られます。

data Expr e where
    Con :: v -> Expr v
    And :: Expr Bool -> Expr Bool -> Expr Bool

いくつかの値の例：

expr1 :: Expr Int
expr1 = Con 42
expr2 :: Expr Bool
expr2 = Con True
expr3 :: Expr Bool
expr3 = Con False
expr4 :: Expr Bool
expr4 = And (Con True) (Con True)
expr5 :: Expr
expr5 = And (Con True) (And (Con False) (Con False))

繰り返しになりますが、に相当するものexpr6はタイプチェッカーを通過しません。これはですがAnd (Con True) (Con 42)、でCon 42あるExpr Intため、の引数として使用することはできません。これは。Andである必要がありますExpr Bool。

これで、評価者は本当に簡単になります。（覚えExpr eておいてください、これはタイプの値を持つ式であることを意味しeます）それは。を返しますe。定数式の値は定数自体であり、論理式の値はオペランドの値の「および」であり、これらの値はBoolsであると確信しています。これは与える：

est :: Expr e -> e
est (Con v) = v
est (And e1 e2) = let b1 = est e1 -- this will be a Bool, since e1 is an Expr Bool
                      b2 = est e2 -- likewise
                  in b1 && b2

指定したGADTは、型指定Exprされていないのと直接同等であり、それでも、などの「不正な」値を作成できますAnd (Con (BoolValue True)) (Con (IntValue 42))。

'Value'型を取り除くことにより、式の型が何であるかをより正確に述べることができます。「式の型は整数またはブール値ですが、まだわかりません」と言って式を評価するときに問題が発生するのではなく、式の値の型を最初から知っていることを確認します。そして、意味をなさない方法でそれらを組み合わせないこと。

これまでに達成できたことを願っています。さまざまなレベルのすべてのタイプ、値、および式が混乱する可能性があります。Expr-そして、タイプとエバリュエーターを自分で拡張して少し実験できるようになります。

簡単に試すことができるのは、文字列または文字定数を使用して2つの整数値を加算する式を作成するか、ブール型の最初の型と同じものの2番目と3番目の3つの引数を取る'if-then-else'式を作成することです。タイプ（ただし、そのタイプは、、、Intなど）。BoolChar

于 2012-04-28T10:25:53.783 に答える
2

GADTを使用するポイントは、すべての式が構造によって適切に型指定されていることを確認することです。これは、があれば、Expr Intそれが適切に型指定されており、に評価されることを意味しますInt。

これを強制するには、定数式がそれらに含まれる型でタグ付けされていることを確認する必要があります。これにより、そのCon 0型はExpr IntwhileCon TrueですExpr Bool。

Con :: v -> Expr v

同様に、がにAnd評価される式でのみ使用できることを確認する必要がありますBool。

And :: Expr Bool -> Expr Bool -> Expr Bool

このように、定数は。が必要な間Con 0 `And` Con 1は型を持っているので、のようなものはコンパイルすらしません。Expr IntAndExpr Bool

これを正しく設定したら、実装est :: Expr e -> eは簡単な作業になるはずです。

于 2012-04-28T09:53:15.163 に答える