私は、Haskellでシングルトンタイプを正しく考えて使用していますか？

Question

いくつかの互換性のないデータ・タイプを作成したいとします。つまり、私は実際にaが何であるかについてを気にすることなくパラメータ化された型Foo a、および、そのような

bar :: (Foo a) -> (Foo a) -> (Foo a) 

としての機能を持っているしたいと思います。およそIntとChar（私は、彼らが同じじゃないことを気にし）同時に、私は本当に気にしませんが、さらに明確にするために、私は

x :: Foo Int 
y :: Foo Char 
bar x y 

をやってから私を停止するように型システムが欲しいです。

私の実際のコードでは、与えられた環の多項式の型があります。私は実際には、型システムが多項式をsの多項式でtに加えるのを止めている限り、不定数が何であるかは気にしません。これまでのところ、私は与えられた多項式が終わったどの特定のリングについてケアを行うので、このアプローチはRing部分は完全に自然な感じ型クラスIndeterminateを作成することでこれを解決し、そして

data (Ring a, Indeterminate b) => Polynomial a b 

としての私の多項式タイプをパラメータ化しました。以下に説明するように、Indeterminateの部分については非常に工夫されています。

上記の方法は問題なく機能しますが、問題はありません。特にこの部分：

class Indeterminate a where 
    indeterminate :: a 

data T = T 

instance Indeterminate T where 
    indeterminate = T 

data S = S 

instance Indeterminate S where 
    indeterminate = S 

（など、多分もっと不確定なもの）。それは不思議で間違っているように感じます。基本的に私はIndeterminateのインスタンスにシングルトン（this sense）を要求しようとしています。奇妙な気持ちは、私がこれを間違って攻撃している可能性のある指標です。もう一つは実際のタイプbがしばしば推測できないので（私はPolynomial a bの多くの注釈をつける必要があるという事実ですが、これは奇妙ではありませんが厄介です）。

提案がありますか？私はちょうどこれのようにそれを続けなければならない、または私は何かを逃している？

PS：すぐにアップヴォートしたり受け入れたりしないと怒らないでください。私は数日間チェックインできません。

Answer 1

まず第一に、私はこのわからない：

data (Ring a, Indeterminate b) => Polynomial a b 

...あなたはそれが何を期待やっています。 dataのコンテキストは非常に有用ではありません。何らかの理由でthe discussion hereを参照してください。なぜなら、実際に多くの追加の型保証を追加することなく余分な注釈を追加する必要があるからです。

第2に、実際には、型が区別されていることを保証する以外の「不確定」パラメータが気になりますか？そのようなことを行うためのかなり標準的な方法は、phantom typesと呼ばれ、データコンストラクタでは使用されない型コンストラクタのパラメータです。もしあなたが望むような機能が多型となることができますので、例えばファントム型の値を使用しないか、必要なんでしょう：

data Foo a b = Foo b 

foo :: Foo a b -> Foo a b 
foo (Foo x) = Foo x 

bar :: Foo a c -> Foo b c 
bar (Foo x) = Foo x 

baz :: Foo Int Int -> Foo Char Int -> Foo() Int 
baz (Foo x) (Foo y) = Foo $ x + y 

明らかにこれは注釈を必要としませんが、唯一のあなたが故意に制限を追加している場所で。そうでなければ、推論はファントム型のパラメータに対して正常に機能します。

シングルトンタイプのビジネスは、複雑なタイプレベルのものと通常のバリューレベルの計算とのギャップを埋めることが主な目的です値のプロキシを入力します。これは、例えば、基底を示す型のベクトルをマーキングするか、または物理的な単位で数値をマーキングする場合に便利です。注釈の意味が単なる「不確定なXというよりも意味がある」場合もあります。