新しいタイプを導入するHaskell関数を作成するには？

Question

私は現在、式パーサーを書いています。私は、字句解析と構文解析を行いましたが、今ではタイプをチェックしています。私はこの（簡易版）のようなデータstructireで式を持っている：

data Expr = EBinaryOp String Expr Expr 
      | EInt Int 
      | EFloat Float 

そして今、私は新しいタイプにこれを変換します機能を必要とし、また、型情報が含まれますTypedExprを、言います。そして今私の主な問題は、このタイプがどのように見えるかです。

data TypedExpr t = TEBinaryOp (TBinaryOp a b t) (TExpr a) (TExpr b) 
       | TEConstant t 
addTypes :: (ExprType t) => Expr -> TypedExpr t 

またはなし：：

data TypedExpr = TEBinaryOp Type BinaryOp TypedExpr TypedExpr 
       | TEConstant Type Dynamic 
addTypes :: Expr -> TypedExpr 

このアプローチは、あなたが式の型を知っていることを前提としているので、私は最初のオプションで始めたが、私は問題に走った型パラメータを持つ - 私は2つのアイデアを持っていますそれを解析する前に（私にとっては、ほとんどの場合そうですが、必ずしもそうではありません）。しかし、私はHaskellの型システムを使用し、コンパイル時に大部分のエラーをチェックできるので、好きです。

最初のオプションで行うことはできますか？
どちらを選択しますか？どうして？
各オプションにはどのような問題がありますか？あなたは、実行時に解析をやっているので

Answer 1

あなたの関数の型、それはあなたがを好きt任意のためのTypedExpr tを得ることを意味するので、

addTypes :: Expr -> TypedExpr t 

は、間違っています。対照的に、あなたが実際に望むのはです。tは、タイプExprの引数で決まります。

この推論は、あなたがHindley-Milnerタイプシステムの機能を超えていることを既に示しています。結局のところの戻り値タイプはaddTypesで、引数の値に依存しますが、Haskell 2010では、値は値に依存しない可能性があります。したがって、従属タイプに近づくタイプシステムの拡張が必要です。ハスケルでは、一般化された代数データ型（GADTs）がそうすることができます。

GADTの最初の紹介については、my video on GADTsも参照してください。

しかし、GADTに精通した後も、型指定されていない表現を型指定された表現に解析するという問題があります。もちろん

addTypes :: Expr -> (exists t. TypedExpr t) 

関数を記述するために、あなたは自分自身をチェックし、いくつかの種類を実行する必要がありますが、それでも、（値のレベルで起こる）あなたのタイプのチェックが可能Haskellのコンパイラを説得することは容易ではありませんタイプレベルに上がった。

エドワードKmett：幸いなことに、他の人がすでに例えばHaskellのカフェメーリングリストに次のメッセージを参照してください、それについて考えています。
Re：GADTの読み取りインスタンスを提供する手動タイプチェック。 は（REました：[Haskellのカフェ] GATDのインスタンスを読む）
http://article.gmane.org/gmane.comp.lang.haskell.cafe/76466

（誰が正式に公開/きれいに書かれた参照を知っていますか？）

Answer 2

、時間をコンパイルしていない、あなたは（あなたは、関連するモジュールをインポートしない限り、手動で自分でそれを呼び出す。）Haskellの型システムのオフにピギーバックすることはできません

あなたが望むことインスピレーションのための単純なラムダ計算のためのタイプチェッカーのTAPLのMLの例に目を向ける。 http://www.cis.upenn.edu/~bcpierce/tapl/（実装中）。ラムダをサポートしていないので、彼らはあなたの表現パーサよりも少しだけ機能します。

Answer 3

を私は最近tagless-final syntaxを使用して開始しています埋め込み型DSLを使用していましたが、私はそれが標準的なGADTメソッド（Apfelmusについて説明しています）よりもずっと良いと判断しました。

tagless-final構文のキーは、式データ型を使用する代わりに、操作を型クラスで表すことです。私は別のBinaryOp関数を作るのではなくかかわらず、文字列を使用することになり

class Repr repr where 
    eInt :: repr Int 
    eFloat :: repr Float 

class Repr repr => BinaryOp repr a b c where 
    eBinaryOp :: String -> repr a -> repr b -> repr c 

：あなたの eBinaryOpのような機能のために、私はそれが最善の2つのクラスを使用することを発見しました。 Oleg's web pageには、Haskellのタイプシステムを使用するパーサーなど、さらに多くの情報があります。