Haskellのパス依存型

Question

私はHaskellの一部のデータベースシステムのAPIを設計しようとしています。このテーブルの列間の相互作用が混ざり合わないようにこのデータベースの列をモデル化したいと思います。

より正確には、あなたには、いくつかのタイプに関連付けられているデータベース内のテーブルを表現するタイプ、持っていることを想像：

type Table a = ... 

、あなたがの種類と一緒に、テーブルの列を抽出することができますように列：

type Column col = ... 

最後に、さまざまな抽出プログラムがあります。あなたのテーブルにはカエルの記述が含まれている場合たとえば、関数は、カエルの重量を含む列を抽出してみましょうになります。ここでは

extractCol :: Table Frog -> Column Weight 

は質問です：私はそのよう列の起源を区別したいと思いますユーザーは表間で操作を実行できません。たとえば：

bullfrogTable = undefined :: Table Frog 
toadTable = undefined :: Table Frog 
bullfrogWeights = extractCol bullfrogTable 
toadWeights = extractCol toadTable 
-- Or some other columns from the toad table 
toadWeights' = extractCol toadTable 
-- This should compile 
addWeights toadWeights' toadWeights 
-- This should trigger a type error 
addWeights bullfrogWeights toadWeights 

私は（[1]参照、パス依存型を使用して）Scalaでこれを実現する方法を知っている、と私はHaskellの中に3つのオプションのことを考えてきた：

• ありません（現在のソリューション）

• テーブルタイプ自体にファントムタイプを追加するためのTypeInType拡張機能を追加し、この余分なタイプを列に渡します。そのような型の構築は非常に複雑なので（テーブルは複雑なDAG操作によって生成される）、このコンテキストではコンパイルが遅くなる可能性があるため、私はそれに熱心ではありません。

  forallの構造をSTモナドと似ていますが、私の場合は余分なタギングタイプが実際に構造を逃れることを望みます。

は、私は同じ列の建設のための非常に限られ、有効なスコープを持って幸せです（つまりtableと(id table)からの列は混合可能でない）、と私はほとんどのではなく、APIのDSL感を気に安全性。ここで

[1] What is meant by Scala's path-dependent types?

私の現在のソリューション

はRankNTypesを使用して、私がやってしまったものです。

強力なタイプチェックをしなくても、ユーザーが適切に見えるように列を使用できるようにしたいと考えています。これは強力な型保証が必要な場合にオプトインします。これはデータの科学者が力を知らないDSLですHaskellの側の

テーブルは、まだその内容によってタグ付けされています

type Table a = ... 

および列は、今そこに含まれるデータの種類の上に、いくつかの余分な参照型でタグ付けされています

type Column ref col = ... 

テーブルからカラムへの投影は、タグ付きまたはタグなしのいずれかです。実際には、これはレンズのようなDSLの後ろに隠されています。

extractCol :: Table Frog -> Column Frog Weight 

data TaggedTable ref a = TaggedTable { _ttTable :: Table a } 

extractColTagged :: Table ref Frog -> Column ref Weight 

withTag :: Table a -> (forall ref. TaggedTable ref a -> b) -> b 
withTag tb f = f (TaggedTable tb) 

今、私は次のようにいくつかのコードを書くことができます。

let doubleToadWeights = withTag toadTable $ \ttoadTable -> 
    let toadWeights = extractColTagged ttoadTable in 
    addWeights toadWeights toadWeights 

し、必要に応じて、これは、コンパイルされません。

let doubleToadWeights = 
    toadTable `withTag` \ttoads -> 
    bullfrogTable `withTag` \tbullfrogs -> 
     let toadWeights = extractColTagged ttoads 
      bullfrogWeights = extractColTagged tbullfrogs 
     in addWeights toadWeights bullfrogWeights -- Type error 

DSLの観点から、私はそれがないようであると考えているがScalaで何が達成できるのかは簡単ですが、タイプエラーメッセージは理解できます。これは私にとって非常に重要です。

Answer 1

ハスケルは（私が知る限りは）パスに依存する型を持っていませんが、ランク2型を使用するといくらかの方法が得られます。

newSTRef :: a -> ST s (STRef s a) 

しかしSTRefます：あなたはSTRefを持つことができるSTのアクション内

runST :: (forall s . ST s a) -> a 

：例えばSTモナドはダミー型runSTの呼び出しの間の漏れを防止するために使用されるパラメータsを持っていますgetはsタイプのパラメータを持ちますので、runSTから逃げることはできません。