다음 코드의 유형 체킹하지 않는 부분지도

Question

와 주문 로케일을 사용하여 : 왜 그렇게

Type unification failed: No type arity option :: order 

Type error in application: incompatible operand type 

Operator: mono :: (??'a ⇒ ??'b) ⇒ bool 
Operand: f :: (char list ⇒ val option) ⇒ char list ⇒ val option 

:

type_synonym env = "char list ⇀ val" 

interpretation map: order "op ⊆⇩m :: (env ⇒ env ⇒ bool)" "(λa b. a ≠ b ∧ a ⊆⇩m b)" 
by unfold_locales (auto intro: map_le_trans simp: map_le_antisym) 

lemma 
    assumes "mono (f :: env ⇒ env)" 
    shows "True" 
by simp 

이사벨이 보조 정리에서 다음과 같은 오류와 함께 불평? 나는 그 해석을 사용할 무언가를 놓쳤는가? 여기에 newtype 래퍼 같은 것이 필요할 것 같습니다 ...

Answer 1

형식 클래스에 해당하는 order과 같은 로캘을 해석 할 때 사용자는 해당 로캘의 컨텍스트 내에서 입증 된 정리 만 얻습니다. 그러나 상수 mono은 형식 클래스에서만 정의됩니다. 그 이유는 mono의 유형에는 두 개의 유형 변수가 포함되는 반면 유형 클래스의 로케일에서는 하나만 사용할 수 있기 때문입니다. 당신의 해석에서 기인하는 map.mono이 없기 때문에 이것을 알 수 있습니다. 당신이 None 미만 Some x 인과 옵션 유형에 대한 유형 클래스 order를 인스턴스화하는 경우 함수 공간이 점별 순서로 order를 인스턴스화하기 때문에

, 당신은,지도에 대한 mono를 사용할 수 있습니다. 그러나,지도상에서의 <=의 순서는 구문 적으로는 ⊆⇩m과 의미 론적으로 동일하므로, ⊆⇩m에 관한 기존의 정리 중 어느 것도 <=으로 작동하지 않으며 그 반대도 마찬가지입니다. 또한, 귀하의 이론은 option에 대해 order을 인스턴스화하는 다른 사람들과 호환되지 않습니다.

따라서 유형 클래스없이 사용하는 것이 좋습니다. 술어 monotone은 명시 적으로 사용 명령을받습니다. 이것은 좀 더 글쓰기는하지만, 결국에는 타입 클래스보다 융통성이 있습니다. 예를 들어 monotone (op ⊆⇩m) (op ⊆⇩m) f을 쓰면 f은 환경의 모노톤 변환이라고 표현할 수 있습니다.