Haskellの入力値に基づいてタイプを制限するにはどうすればよいですか？

Question

私はハスケルを新しくしました。申し訳ありませんが、この質問に明らかな答えがある場合。

私はiとjは任意Intのある A (Baz i) (Baz j)以外Tmpのための任意のコンストラクタを取ることができA Tmp Tmpコンストラクタ

data Tmp = Foo Int 
     | Bar Int 
     | Baz Int 

と

data Test = A Tmp Tmp 

を持っています。何か方法がありますか TmpのA Tmp Tmpは、最初にTmpがある場合はBazになります。Baz？

Answer 1

答えは、制限をどのように強制するかによって異なります。実行時またはコンパイル時。

制限を実行時にに適用するには、制限をチェックしてからコンストラクタを呼び出す関数（たとえば、makeA）を追加できます。いくつかの処理を行い、次にコンストラクタを呼び出す関数はスマートコンストラクタとも呼ばれます。スマートコンストラクタmakeAのみをエクスポートし、モジュールから実際のコンストラクタAをエクスポートしない場合は、他のモジュールがスマートコンストラクタを使用していることを確認することができます。

例：

module Test (Tmp (Foo, Bar, Baz), Test(), makeA) where 
    data Tmp 
    = Foo Int 
    | Bar Int 
    | Baz Int 

    data Test = A Tmp Tmp 

    makeA :: Tmp -> Tmp -> Tmp 
    makeA (Baz _) (Baz _) = error "makeA: two baz problem" 
    makeA tmp1 tmp2 = A tmp1 tmp2 

この手法の利点は、あなたがすべてのあなたのデータ型を変更する必要がないことです。欠点は、制限が実行時にのみ強制されることです。

コンパイル時に制限を適用するには、のデータ型を何らかの形で変更する必要があります。現在のデータ型の問題は、型チェッカーがFooとBarで構成された値とBazで構成された値を区別できないことです。型チェッカーでは、これらはすべてTmpの値であるため、型チェッカーではTmpの値は大丈夫、他の値は正しくないことを強制できません。したがって、型の中のTmp値の "Bazness"をエンコードするようにデータ型を変更する必要があります。タイプでBaznessを符号化するための

1つのオプションは、次のようにTmpを再構築するために、次のようになります。

data TmpNotBaz 
    = Foo Int 
    | Bar Int 

data Tmp 
    = NotBaz TmpNotBaz 
    | Baz Int 

今ではタイプTmpNotBazの値がBazが、タイプTmpの値ではないことは明らかですBazとすることができます。このアイデアの利点は、基本的なHaskellの機能しか使用していないことです。ちょっとした欠点は、NotBazへの呼び出しをコードに入れる必要があることです。大きな欠点は、「Aの引数のうちの1つがBazになる可能性がある」という考えを直接表現することができないことです。私たちは、Aの複数のバージョンを記述する必要があります：

data Test 
    = A1 TmpNotBaz Tmp 
    | A2 Tmp TmpNotBaz 

今、私たちは、必要に応じてA1またはA2を選択することで、私たちが望むすべての値を表現することができ、必要に応じて、我々は、もうA (Baz ...) (Baz ...)を表現することはできません。このソリューションの問題は、以前のものに対して複数の表現があることです。例えば、A (Foo 1) (Foo 2)：A1 (Foo 1) (NotBaz (Foo 2))とA2 (NotBaz (Foo 1)) (Foo 2)の両方がこの値を表します。

このようなデータ型の構造で遊んでみて、自分の状況に適したバージョンを作成できます。

Tmpタイプにタイプ・レベル情報のビットに注釈を付けると、このタイプのレベルの情報について推論する型レベルのプログラミングを使用することであろう型にBaznessを符号化するための別のオプション。このアイデアの欠点は、より高度なHaskellの機能を使用していることです。実際には、この種のことを行うための新しい方法が数多くありますが、どれが「標準的な」高度なHaskellとみなされるのかは不明です。

{-# LANGUAGE GADTs, TypeFamilies, DataKinds #-} 

data Bazness = IsBaz | NotBaz 

data BothBazOrNot = BothBaz | NotBothBaz 

type family AreBothBaz (b1 :: Bazness) (b2 :: Bazness) :: BothBazOrNot where 
    AreBothBaz 'IsBaz 'IsBaz = 'BothBaz 
    AreBothBaz _ _ = 'NotBothBaz 

data Tmp (b :: Bazness) :: * where 
    Foo :: Int -> Tmp 'NotBaz 
    Bar :: Int -> Tmp 'NotBaz 
    Baz :: Int -> Tmp 'IsBaz 

data Test where 
    A :: AreBothBaz b1 b2 ~ 'NotBothBaz => Tmp b1 -> Tmp b2 -> Test 

注どのようにコンストラクタがIsBazまたはNotBaz何かを作成するかどうかについてのコンストラクタの型シグネチャはFoo、BarとBaz話：それは言った、ここで一つのアプローチです。そして、どのようにAの型署名がb1とb2という選択肢について話しているので、NotBothBazになります。

• A (Foo 1) (Bar 2)
• A (Foo 1) (Baz 2)
• A (Baz 1) (Bar 2)

をしかし、我々はA (Baz 1) (Baz 2)を書くしようとした場合、型チェッカーは文句：：

このコードを使用して、我々は次の式を書くことができ

を

Couldn't match type 'BothBaz with 'NotBothBaz 
    arising from a use of A 
In the expression: A (Baz 1) (Baz 2) 

だから、型チェッカーは、この場合には、Aへの引数はBothBazですが、我々はNotBothBazの引数を受け入れるだけにAの種類を注釈付きなので、型チェッカーがBothBazがNotBothBaz異なっていることを訴えることを考え出しました。