하스켈의 Existential types 타입 오류

Question

내 프로그램의 실존 타입에 어려움을 겪고 있습니다. 나는 모나드

data M o = R o | forall o1. B (o1 -> M o) (M o1) 

지금 나는 그것을위한 컨텍스트를 만들 모방의 종류, 유사한 데이터 유형을 가지고 내가 그러나 나는 typechecker :(

과거 얻을 수없는 매우 합리적인 뭔가를 할 노력하고있어 생각 그 Haskell Wiki article on Zipper 설명에, 그러나 나는 단순함에 대한 데이터 구조 대신 함수를 사용 -

type C o1 o2 = M o1 -> M o2 

을 지금은 그 상황과 하위 값에 데이터 값을 분할하는 함수를 작성하려고하면 typechecker는 불평 -

ctx :: M o -> (M o1 -> M o, M o1) 
ctx (B f m) = (B f, m) -- Doesn't typecheck 

오류입니다 - 그러나

Couldn't match type `o2' with `o1' 
    `o2' is a rigid type variable bound by 
     a pattern with constructor 
     B :: forall o o1. (o1 -> M o) -> M o1 -> M o, 
     in an equation for `ctx' 
     at delme1.hs:6:6 
    `o1' is a rigid type variable bound by 
     the type signature for ctx :: M o -> (M o1 -> M o, M o1) 
     at delme1.hs:6:1 
Expected type: M o2 
    Actual type: M o1 
In the expression: m 
In the expression: (B f, m) 

, 정말처럼 해결할 수 있습니다 -

ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK 

왜이 두 번째 정의의 유형 체킹하지만이 첫 번째합니까? 나는 R를 확인하여 완전한 기능 ctx를 변환 할 경우

또한, 나는 다시 유형 체킹이 오류가 -

ctx (R o) = (id, R o) -- Doesn't typecheck 

오류 - 나는이 문제를 해결할 수있는 방법

Couldn't match type `o' with `o1' 
    `o' is a rigid type variable bound by 
     the type signature for ctx :: M o -> (M o1 -> M o, M o1) 
     at delme1.hs:7:1 
    `o1' is a rigid type variable bound by 
     the type signature for ctx :: M o -> (M o1 -> M o, M o1) 
     at delme1.hs:7:1 
In the first argument of `R', namely `o' 
In the expression: R o 
In the expression: (id, R o) 

오류?

도움을 주시면 감사하겠습니다.

Answer 1

먼저 실패한 사례를 살펴 보겠습니다. 이들 모두는 유형 서명에 암시 적 forall에 추가하면 명확 같은 이유로, 실패 :

ctx :: forall o o1. M o -> (M o1 -> M o, M o1) 

즉 함수해야합니다 일부 o1에 대한뿐만 아니라 작동하지만 어떤o1합니다. 첫 번째 경우

1. ,

   ctx (B f m) = (B f, m) 
   

   우리가 알고 우리가 어떤 유형 o1을 제공 할 수 있도록, 그래서 우리가 할 수있는 일부 유형 o2,뿐만 f :: (o2 -> M o) 및 m :: M o2, 그 o1 ~ o2이라고 가정합니다. 두 번째 경우

2. , 여기

   ctx (R o) = (id, R o) 
   

   , 우리는 o :: o는, 그러나 다시, 함수가 어떤o1에 대해 정의되어야 함을 알고, 그래서 우리는 o ~ o1 있다고 가정 할 수 없다.

해결 방법은 귀납적 증거와 마찬가지로 자체를 호출하기 때문에 작동하는 것 같습니다. 그러나 기본 케이스가없는 경우, 그것은 단지 순환 추론 일 뿐이며, 하단 값을 사용하지 않고 o과 o1의 조합에 대해 M o에서 M o1을 구성 할 방법이 없으므로이 함수의 기본 사례를 작성할 수 없습니다.

튜플 만 사용하는 대신 컨텍스트에 대해 다른 실존 유형을 정의하는 것이 좋습니다. 아니 그것은 당신의 필요에 따라 작동 있을지 모르겠지만,이 적어도 ¹을 컴파일 :

data Ctx o = forall o1. Ctx (M o1 -> M o) (M o1) 

ctx :: M o -> Ctx o 
ctx (B f m) = case ctx m of Ctx c m' -> Ctx (B f . c) m' 
ctx (R o) = Ctx id (R o) 

_{¹a funny GHC error :}