5

データ型があるとしましょう

data Interval :: Nat -> Nat -> * where
  Go :: Interval m n -> Interval m (S n)
  Empty :: SNat n -> Interval n n

これらは、半分（右）の開区間です。Natは標準的な帰納的自然でSNatあり、対応するシングルトンです。

Natここで、指定された間隔の長さのシングルトンを取得したいと思います。

intervalLength :: Interval n (Plus len n) -> SNat len
intervalLength Empty = Z
intervalLength (Go i) = S (intervalLength i)

Plus関数は単射ではないため、これは機能しません。私はおそらくそれを次のように定義することができます

intervalLength :: Interval m n -> SNat (Minus n m)

しかし、それにはいくつかの見出語（および追加の制約）が必要になると思います。また、私の間隔は前者の形で発生します。

背景：オメガでこれを実行しようとしましたが、機能しませんでした（オメガのバグを提出しました）

また、これらの問題は、変更されたタイプチェッカーでどのように解決できますか？供給のRHSは、非注入性が相殺されるように、LHSパターンのタイプ方程式に重要なヒントを提供できますか？

Agdaプログラマーはこれらの問題にどのように取り組んでいますか？

4

2 に答える 2

13

これが私のバージョンのプログラムです。使っています

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

そして私は持っているNatとそのシングルトン

data Nat = Z | S Nat

data SNat :: Nat -> * where
  ZZ :: SNat Z
  SS :: SNat n -> SNat (S n)

あなたのIntervalタイプは、「以下」の「接尾辞」の定義として私にはよく知られています。「接尾辞」は、数値からリストにアップグレードし、それぞれSに要素のラベルを付けると、次の定義が得られるためです。リストの接尾辞。

data Le :: Nat -> Nat -> * where
  Len :: SNat n -> Le n n
  Les :: Le m n -> Le m (S n)

ここに追加があります。

type family Plus (x :: Nat) (y :: Nat) :: Nat
type instance Plus Z     y  = y
type instance Plus (S x) y  = S (Plus x y)

さて、あなたのパズルは、Lesある値のコンストラクターを数え、Leそのインデックス間の差のシングルトンを抽出することです。いくつかを使用して計算しようとしていると仮定するのではなく、任意のインデックス間の差を計算し、との接続を確立する関数を記述します。Le n (Plus m n)SNat m Le m oPlus

Leシングルトンが提供された、の加法的な定義は次のとおりです。

data AddOn :: Nat -> Nat -> * where
  AddOn :: SNat n -> SNat m -> AddOn n (Plus m n)

Leを意味することを簡単に確立できますAddOn。一部のパターンマッチングは、一部のパターンマッチングであり、必要なシングルトンAddOn n oを提供します。oPlus m nm

leAddOn :: Le m o -> AddOn m o
leAddOn (Len n) = AddOn n ZZ
leAddOn (Les p) = case leAddOn p of AddOn n m -> AddOn n (SS m)

より一般的には、依存型プログラミングの問題を定式化して、一致させる予定の型のインデックスに定義された関数が存在することを最小限に抑えることをお勧めします。これにより、複雑な統合を回避できます。（このような関数を緑色に着色するために使用されるエピグラム、したがって「緑色のスライムに触れないでください！」というアドバイス。）Le n o、それは（それがポイントであるためleAddOn）、より有益なタイプでLe n (Plus m n)あることがわかりますが、それはかなり簡単です一致する。

さらに一般的には、問題のロジックをキャプチャする依存データ型を設定するのはごく普通の経験ですが、操作するのは非常に恐ろしいことです。これは、正しいロジックをキャプチャするすべてのデータ型が絶対に恐ろしく機能することを意味するのではなく、定義の人間工学についてもっと深く考える必要があるということです。これらの定義をきちんと理解することは、多くの人が通常の関数型プログラミングの学習経験で習得するスキルではないため、新しい学習曲線を登ることを期待してください。

于 2012-11-25T22:30:09.733 に答える
8

私はイドリスでこれを試しました。問題を再構築するという pigworker の提案には同意しますが、定義を Idris 型チェッカーを通過させるには、次のことを行う必要があります。まず、シングルトン Nats:

data SNat : Nat -> Set where
   ZZ : SNat O
   SS : SNat k -> SNat (S k)

次に、間隔の定義:

data Interval : Nat -> Nat -> Set where
  Go : Interval m n -> Interval m (S n)
  Empty : SNat n -> Interval n n

intervalLength に必要な定義は、次のようになります。

intervalLength : Interval n (plus len n) -> SNat len
intervalLength (Empty sn) = ZZ
intervalLength (Go i)     = SS (intervalLength i)

plusしかし、あなたが言うように単射ではないので、あなたはトラブルに遭遇するでしょう. 明示的にパターンマッチングを追加することで、どこかを取得できますlen-そうすれば、統合がいくらか進歩する可能性があります:

intervalLength : Interval n (plus len n) -> SNat len
intervalLength {len = O}   (Empty sn) = ZZ
intervalLength {len = S k} (Go i)     = SS (intervalLength i)

これは問題なく、タイプチェッカーを通過しますが、残念ながら、関数が完全であるとは信じていません。

*interval> :total intervalLength
not total as there are missing cases

欠落しているケースは次のとおりです。

intervalLength {len = O}   (Go i)     = ?missing

これを試して、REPL に のタイプを尋ねると、次のようにmissing表示されます。

missing : (n : Nat) -> (i : Interval (S n) n) -> SNat O

これで、型が空であることがわかりましたInterval (S n) nが、残念ながら、型チェッカーはそうではありません。どういうわけか と書く必要がありbadInterval : Interval (S n) n -> _|_、次のように言えます。

intervalLength {len = O}   (Go i)     = FalseElim (badInterval i)

の定義はbadInterval練習問題として残しておきます:-)。特にトリッキーではありませんが、やらなければならないことは少し退屈です - 時々、この種の型を使わなければならないことを避けるのは難しいですが、実装は、このようにbadIntervalしないという豚労働者の提案をバックアップします!

于 2012-11-25T23:26:18.117 に答える