Idris：有限両用の算術

Question

私はIdrisを初めて利用しています。私は有界数を記述するデータを作成する必要があります。だから私は、このようなコンストラクタで、このようなデータを作りました：

data BoundedDouble : (a, b : Double) -> Type where 
    MkBoundedDouble : (x : Double) -> 
        {auto p : a <= x && x <= b = True} -> 
        BoundedDouble a b 

Doublea間とbを作成しているようです。 これは簡単な使用例です：

test : BoundedDouble 0.0 1.0 
test = MkBoundedDouble 0.0 

これは動作します。しかし、今私はBoundedDoubleのためのNumインターフェイスを実装したいと思います。

Num (BoundedDouble a b) where 
    (MkBoundedDouble x) + (MkBoundedDouble y) = 
    MkBoundedDouble (ifThenElse (x + y > b) 
         (x + y - (b - a)) 
         (ifThenElse (x + y < a) 
         (x + y + (b - a)) 
         (x + y))) 

しかし、それは動作しません、私はなぜ推測するが、私はそれを説明することはできません：私はこれを試してみました。 追加はどのように実装する必要がありますか？

私はそれを理解するために何をすべきか、読むべきかどうかはわかりません。

Answer 1

ここには2つの問題があります。 Double arithmetic is defined with primitive functions.イドリスはa <= b = True -> b <= c = True -> a <= c = Trueを証明することさえできません。（これはすべての時間を保持していないので、これはIdrisのせいではありません）a <= b = True以外の証拠はありません。 ifThenElse。

このようなブラインドランタイムプルーフを使用すると（… = True）、Data.Soは非常に役に立ちます。 ifThenElse (a <= x) … …は指定されたブールチェックを分岐しますが、ブランチのコードはチェックの結果については認識しません。 choose (a <= x)では、ブランチの結果はLeft prfとprf : So (a <= x)またはRight prfとprf : So (not (a <= x))となります。

2つの有界2倍を加算した結果が上限より大きい場合、結果はこの上限になるはずです。

import Data.So 

data BoundedDouble : (a, b : Double) -> Type where 
    MkBoundedDouble : (x : Double) 
         -> {auto high : So (a <= x)} 
         -> {auto low : So (x <= b)} 
         -> BoundedDouble a b 

Num (BoundedDouble a b) where 
    (+) (MkBoundedDouble u) (MkBoundedDouble v) = 
      let x = u + v 
      in case (choose (a <= x), choose (x <= b)) of 
      (Left _, Left _) => MkBoundedDouble x 
      (Right _, _) => ?holeMin 
      (_, Right _) => ?holeMax 

これはすでにタイプチェックされていますが、穴が空いています。 ?holeMinをMkBoundedDouble aに、?holeMaxをMkBoundedDouble bに設定します。しかし、今すぐMkBoundedDoubleの2つの証明：highとlowが必要です。 ?holeMaxの場合、それらはx = bSo (a <= b)とSo (b <= b)となります。再び、Idrisは、b : Doubleごとにb <= bを知らない。だから我々は、これらの証明を取得するために再度選択する必要があります：

   (_, Right _) => case (choose (a <= b), choose (b <= b)) of 
        (Left _, Left _) => MkBoundedDouble b 
        _ => ?what 

イドリスはb <= bは、関数は部分的であろうと見ることはできませんので。私たちは不正行為をして?whatにMkBoundedDouble uを使用することができるので、関数はタイプチェックを行い、これが実際には起こらないことを望みます。

b <= bは常に真であることを力で型チェッカーを説得する可能性もあります：

data BoundedDouble : (a, b : Double) -> Type where 
    MkBoundedDouble : (x : Double) 
         -> {auto rightSize : So (a <= b)} 
         -> {auto high : So (a <= x)} 
         -> {auto low : So (x <= b)} 
         -> BoundedDouble a b 

DoubleEqIsSym : (x : Double) -> So (x <= x) 
DoubleEqIsSym x = believe_me (Oh) 

Num (BoundedDouble a b) where 
    (+) (MkBoundedDouble u) (MkBoundedDouble v) = 
      let x = u + v 
      in case (choose (a <= x), choose (x <= b)) of 
      (Left _, Left _) => MkBoundedDouble x 
      (Right _, _) => MkBoundedDouble a {high=DoubleEqIsSym a} 
      (_, Right _) => MkBoundedDouble b {low=DoubleEqIsSym b} 

それとも私たちも、より安全で、データコンストラクタで上限と下限のための証明を置くことができ、そのため、?holeMinと?holeMaxに使用できます。

コンストラクタがプルーフでパックされていても、実装が複雑にならないことがわかります。そして、それらは実際の実行時コードで消去されるべきです。

しかし、練習として、あなたはイドリスのために多くのリソースがまだ存在していない、悲しいこと

data BoundedDouble : (a, b : Double) -> Type where 
    MkBoundedDouble : (x : Double) 
         -> {auto rightSize : So (a <= b)} 
         -> {auto high : So (a <= x)} 
         -> {auto low : So (x <= b)} 
         -> BoundedDouble a b 
    Min : {auto rightSize : So (a <= b)} -> BoundedDouble a b 
    Max : {auto rightSize : So (a <= b)} -> BoundedDouble a b 

ためNumを実装しようとすることができます。チュートリアルの他に、開発中のa bookがあります。私はこれをお勧めします。これは、プリミティブ型で作業するよりも、より親しみやすい演習を提供します。 :-)