관측 유형 이론의 패턴 일치

Question

"전체 OTT"섹션의 끝 부분 인 Towards Observational Type Theory에서 저자는 OTT에서 coercible-under-constructors 색인 데이터 유형을 정의하는 방법을 보여줍니다. 코너는 observational type theory (delivery)의 하단에이 기술을 언급

data IFin : ℕ -> Set where 
    zero : ∀ {n} -> IFin (suc n) 
    suc : ∀ {n} -> IFin n -> IFin (suc n) 

data PFin (m : ℕ) : Set where 
    zero : ∀ {n} -> suc n ≡ m -> PFin m 
    suc : ∀ {n} -> suc n ≡ m -> PFin n -> PFin m 

가

: 다음과 같은 파라미터에 아이디어는 인덱스 데이터 유형을 설정하는 기본적

수정, 물론,이해야 할 무엇 GADT 사람들은 명시 적 평등에 대해 명시 적으로 유도 가정을 정의합니다. 그리고 나서 물론 transisitivity에 의해 그들을 수송 할 수 있습니다.

그러나 Haskell의 유형 검사기는 범위의 동일성 제약 조건을 인식하고 실제로 유형 검사 중에이를 사용합니다. 예 : 그것은 유형 이론에 그렇게 작동하지 않습니다

f :: a ~ b => a -> b 
f x = x 

는이 방정식에 의해 재 작성 할 수있는 범위 내에서 a ~ b의 증거가 충분하지이기 때문에 우리가 쓸 수 있습니다 : 그 증거는, refl해야합니다에 있기 때문에 거짓 가설 유형 검사의 종료는 종료 문제 (this과 같은 것)로 인해 결정 불가능 해집니다. 따라서 Haskell에서 Fin m의 패턴 일치를 m이 각 분기에서 으로 다시 작성하지만 형식 이론에서는 발생할 수 없으며 대신 suc n ~ m이라는 확실한 증거가 남습니다. OTT에서는 교정본에 패턴 매칭을 할 수 없으므로 증명이 refl 인 것처럼 할 수도없고 실제로 요구할 수도 없습니다. 증거를 coerce에 제공하거나 무시할 수 있습니다.

이렇게하면 인덱싱 된 데이터 형식과 관련된 모든 것을 작성하기가 매우 어렵습니다. 예 : (타입 시그니처 포함) 보통 세 라인 벡터의 lookup이 짐승된다 : decidable 동등성을 가지는 데이터 유형의 두 요소가 observably 같으면 보낸 후,

vlookupₑ : ∀ {n m a} {α : Level a} {A : Univ α} -> ⟦ n ≅ m ⇒ fin n ⇒ vec A m ⇒ A ⟧ 
vlookupₑ   p (fzeroₑ q)  (vconsₑ r x xs)  = x 
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vconsₑ {m′} r x xs) = 
    vlookupₑ (left (suc n′) {m} {suc m′} (trans (suc n′) {n} {m} q p) r) i xs 
vlookupₑ {n} {m} p (fzeroₑ {n′} q) (vnilₑ r)   = 
    ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r 
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vnilₑ r)   = 
    ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r 

vlookup : ∀ {n a} {α : Level a} {A : Univ α} -> Fin n -> Vec A n -> ⟦ A ⟧ 
vlookup {n} = vlookupₑ (refl n) 

그것은 다소 단순화 될 수 그들이 는 일반적인 intensional sense와 동일하고 자연수는 결정할 수있는 평등을 갖기 때문에 모든 방정식을 intensional counterparts와 pattern match로 강요 할 수 있습니다. 그러나 이는 vlookup의 일부 계산 속성을 깨고 어쨌든 장황합니다. 평등을 결정할 수없는 지표로 더 복잡한 사례를 다루는 것은 거의 불가능합니다.

제 생각은 정확합니까? OTT의 패턴 매칭은 어떻게 작동합니까? 이것이 실제로 문제가된다면 그것을 완화 할 수있는 방법이 있습니까?

Answer 1

나는 이것을 하나의 필드로 만들 것이다. 나는 이상한 질문을 발견하지만 그것은 내 자신의 특별한 여행 때문입니다. 간단히 대답하면 : OTT 나 커널 유형 이론에서 패턴 매칭을하지 마십시오. 패턴 매칭을하지 않는 것과 같은 것은 아닙니다.

긴 대답은 기본적으로 내 박사 학위 논문입니다.

박사 학위 논문에서 필자는 패턴 매칭 스타일로 작성된 고급 프로그램을 귀납적 데이터 유형에 대한 유도 원칙과 명제 평등에 대한 적절한 처리 만있는 커널 유형 이론으로 정교하게 만드는 방법을 보여줍니다. 패턴 매칭의 정교화는 데이터 유형 인덱스에 대한 명제 방정식을 도입 한 다음 통합을 통해이를 해결합니다. 그 당시에는 내적 평등을 사용했지만 관찰의 평등은 적어도 당신에게 동일한 힘을줍니다.즉 : 패턴 매칭을 정교하게 (그리고 커널 이론에서 벗어나서) 유지하는 나의 기술은 모든 동등한 양동이를 숨기고, 관측 평등으로 업그레이드하기 이전이다. 귀하의 요점을 설명하기 위해 사용한 격렬한 vlookup은 정교화 프로세스의 결과물과 일치 할 수 있지만, 입력이 그렇게 나쁘지는 않습니다. 좋은 정의

vlookup : Fin n -> Vec X n -> X 
vlookup fz  (vcons x xs) = x 
vlookup (fs i) (vcons x xs) = vlookup i xs 

잘 정교합니다. 그 과정에서 발생하는 방정식 해결은 Agda가 패턴 매칭을 통해 정의를 검사 할 때 또는 하스켈이 수행 할 때 메타 수준에서 수행하는 방정식 해결과 동일합니다.

f {q} x = coerce q x 

일종의 부연하지만 당신의 얼굴에없는 그, 커널 하스켈에서

f :: a ~ b => a -> b 
f x = x 

같은 프로그램에 속지 마십시오. 그리고 그것은 컴파일 된 코드가 아닙니다. Haskell 항등 증명과 같은 OTT 항등 증명은 을 사용하여 계산하기 전에 지울 수 있으며 항을 닫습니다.

소송. 하스켈 평등 데이터의 상태에 대한 명확하게하기 위해, GADT

data Eq :: k -> k -> * where 
    Refl :: Eq x x 

정말 당신에게

Refl :: x ~ y -> Eq x y 

을 제공하지만, 타입 시스템은 논리적으로 소리하지 않기 때문에, 형 안전 엄격한 패턴에 일치에 의존 그 유형 : 당신은 Refl을 지울 수 없다. 그리고 당신은 정말로 그것을 계산해야하고, 실행 시간에 일치 시켜야만한다. 그러나 은 이라는 증거에 해당하는 데이터를 지울 수있다.. OTT에서, 전체 명제 단편은 공개 용어에 대해서는 부적절하고 닫힌 계산에는 지울 수 있습니다. 끝 부분.

이 데이터 유형에 대한 평등의 결정 가능성은 특별히 관련이 없습니다 (최소한 ID 증명의 고유성이있는 경우가 아니라 UIP가 항상있는 것은 아니지만 결정 가능성은 때로는 얻을 수있는 한 가지 방법입니다). 패턴 매칭에서 나타나는 균등 문제는 임의로 표현식에 있습니다. 그것은 많은 로프입니다. 그러나 기계는 변수와 완전히 적용된 생성자로 구성된 1 차 표현식으로 구성된 단편을 확실하게 결정할 수 있습니다 (Agda가 사례를 분할 할 때 Agda가 수행하는 것 : 제약 조건이 너무 이상한 경우 바보입니다). OTT는 우리가 고차원 통일의 결정적인 단편으로 조금 더 나아갈 수 있도록해야한다. 알 수없는 경우 을 알고있는 경우 f은 f = \ x -> t[x]과 같습니다.

그래서 OTT에서 패턴 일치는 항상 의도적 인 디자인 선택이었습니다. 우리는 이미 수행 방법을 알고있는 번역을위한 정교화 대상이었습니다. 오히려 그것은 커널 이론의 힘을 엄격하게 업그레이드 한 것입니다.