タイプのコンストラクタのサブセットのみを受け付ける関数を作成するにはどうすればよいですか？

Question

だが、私はこのようなタイプがあるとしましょう：

data Foo = Bar String | Baz | Qux String 

私はこのような機能を持つようにしたい：欠落している場合があるように記述したよう

get : Foo -> String 
get (Bar s) = s 
get (Qux s) = s 

を、これはコンパイルが、それはトータルではありません;言い換えれば、get Bazは型チェックされない式ではなく穴のように扱われます。

タイプシグニチャgetのFooを、BarまたはQuxのいずれかにする必要があることを指定するものに置き換えます。 Fooタイプのこのサブセットを表現するにはどうすればよいですか？

Answer 1

あなたはまた、二つのアプローチを混ぜることができ（でKim Stiebel、Anton Trunov）を作成し、ヘルパーデータ型を構築します。タイプOnlyBarAndQuxは、BarとQuxの値でのみ構成できます。イドリスにとっては、これはgetを起動する場合がある場合は、自動的に証明を推測することが可能である：

module FooMe 

data Foo = Bar String | Baz | Qux String 

data OnlyBarAndQux: Foo -> Type where 
    BarEy: OnlyBarAndQux (Bar s) 
    QuxEx: OnlyBarAndQux (Qux s) 

||| get a string from a Bar or Qux 
total 
get: (f: Foo) -> {auto prf : OnlyBarAndQux f} -> String 
get (Bar s) {prf = BarEy} = s 
get (Qux s) {prf = QuxEx} = s 

-- Tests 

test1: get $ Bar "hello" = "hello" 
test1 = Refl 

test2: get $ Qux "hello" = "hello" 
test2 = Refl 

-- does not compile 
-- test3: get $ Baz = "hello" 

Answer 2

あり、これを行うために複数の方法がありますが、最も簡単には、それはそれでStringかとFooだかどうかを示すパラメータを取りFoo型コンストラクタを作るために、おそらくです。 （@EduardoパレハTobesによって観察されるようFooを変更すると、オプションの場合）私はキムStebelの答えと一緒に行きたい

%default total 

data Foo : Bool -> Type where 
    Bar : String -> Foo True -- a Foo constructed with Bar will have type Foo True 
    Baz : Foo False -- and a Foo constructed with Baz will have type Foo False 
    Qux : String -> Foo True 

get : Foo True -> String 
get (Bar s) = s 
get (Qux s) = s 

Answer 3

が、私はしたいと思います。この例では、私は、パラメータとしてBoolを使用していました別の方法を示します。

total 
get : (f ** Not (f = Baz)) -> String 
get (f ** pf) with (f) 
    get (f ** _)  | (Bar s) = s      -- this is as before 
    get (f ** contra) | Baz = void $ contra Refl   -- a contradictory case 
    get (f ** _)  | (Qux s) = s      -- this is as before 

(f ** Not (f = Baz))は「いくつかのタイプFooのfはなく、Baz」として翻訳することができます：あなたは依存ペアと同じものであるサブセットのタイプを、使用することができます。

あなたがそうのように、タイプFooの要素と、それはBazと等しくないことを証明の依存ペアを提供する必要がget呼び出すに：

s : String 
s = get (Bar "bar" ** \Refl impossible) 

Answer 4

私は、たとえば、List headためのstdライブラリで撮影したアプローチに従うと思います。

%default total 

data Foo = Bar String | Baz | Qux String 

data NotBaz : Foo -> Type where 
    IsBar: NotBaz(Bar z) 
    IsQux: NotBaz(Qux z) 

Uninhabited (NotBaz Baz) where 
    uninhabited _ impossible 

notBaz : (f : Foo) -> Dec (NotBaz f) 
notBaz Baz  = No absurd 
notBaz (Bar s) = Yes IsBar 
notBaz (Qux s) = Yes IsQux 

get: (f : Foo) -> {auto ok : NotBaz f} -> String 
get (Bar s) { ok = IsBar } = s 
get (Qux s) { ok = IsQux } = s 

s: String 
s = get (Bar "bar") 

このことについていくつかのコメント：

1. 一緒に働くためにだけ述語a -> Boolを使用しないでくださいこれは、基本的に何Markus wroteプラスFooがBazでないということを目の当たりにためDecを使用して決定可能ですサブセットタイプa; ビュー、上記のようにNotBazを作成してください。コンテキストについてはthe Idris tutorial on views,this postおよびthis answerを参照してください。
2. 可能であれば、同等性の代わりにDecを使用してください。洞察的には、Decを、明示的にと指定できるタイプの述部に使用できます。上記のnotBazを参照してください。
3. 自動暗黙の引数は、このアプローチはFoo`良くないと `Foo`がライブラリからインポートされたときのように、不可能であるかもしれない`変更する必要用法サイト