이드리스 : 바운드 더블 용 산도

Question

나는 이드리스를 처음 사용합니다. 바운드 된 숫자를 설명하는 데이터를 만들어야합니다. 그래서 나는 그런 생성자와 같은 데이터를했습니다 :

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

여기에는 두 가지 문제가 있습니다. Double arithmetic is defined with primitive functions. 이드리스는 a <= b = True -> b <= c = True -> a <= c = True을 증명할 수조차 없습니다. (그런데 항상 홀드하지 않습니다. 따라서 이드리스의 잘못이 아닙니다.) 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 개의 bounded double을 더한 결과가 upper bound보다 크면, 결과는이 upper bound이어야한다고 가정합니다. 첫 시도 :

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에는 high과 low의 두 가지 증명이 필요합니다. ?holeMax의 경우에는 x = bSo (a <= b) 및 So (b <= b)이됩니다. 다시 말하지만 Idris는 b : Double에 대해 b <= b을 모릅니다. 그래서 우리는 이러한 증거를 얻기 위해 다시 선택해야합니다 : 이드리스는 b <= b이 함수는 부분이 될 것이라고 볼 수 없습니다

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

때문입니다. 우리는 속이며 ?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에서 사용할 수 있습니다.

import Data.So 

data BoundedDouble : (a, b : Double) -> Type where 
    MkBoundedDouble : (x : Double) 
         -> {auto rightSize : So (a <= b)} 
         -> {auto leftId : So (a <= a)} 
         -> {auto rightId : So (b <= b)} 
         -> {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 _, _) => MkBoundedDouble a 
      (_, Right _) => MkBoundedDouble 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 
    Min : {auto rightSize : So (a <= b)} -> BoundedDouble a b 
    Max : {auto rightSize : So (a <= b)} -> BoundedDouble a b 

에 대한 Num을 구현하기 위해 시도 할 수 있습니다. 튜토리얼 외에 개발 중에는 a book이 있는데, 나는 그것을 권하고 싶다. 기본 유형으로 작업하는 것보다 더 친숙한 연습을 제공합니다. :-)