Data.Void의 터무니없는 기능은 무엇에 유용합니까?

Data.Void의 터무니없는 기능은 무엇에 유용합니까?

---

의 함수 에는 다음 서명 이 있습니다. 여기서는 해당 패키지에서 내에서 보낸 송금으로 무인 유형입니다.absurdData.VoidVoid

-- | Since 'Void' values logically don't exist, this witnesses the logical
-- reasoning tool of \"ex falso quodlibet\".
absurd :: Void -> a

나는 유효한 공식에 대응하는 유형의 명제에 해당하는 문서의 발언을 소유에 논리를 알고 있습니다 ⊥ → a.

제가 궁금하고 궁금한 점은이 함수가 어떤 종류의 실용적인 프로그래밍 문제에서 유용합니까? "일어날 수없는"사례를 철저하게 처리하는 형식 안전 방법으로 어떤 경우에는 유용하게 생각하지만 Curry-Howard의 실제 사용에 대해 충분히 알지 못합니다. 전혀 올바른 길.

편집 : Haskell에서 가급적 예를 들었지만 누군가가 거기에서 입력 된 언어를 사용하고 불평하지 않습니다 ...

---

Haskell은 엄격하지 않기 때문에 삶은 조금 어렵습니다. 일반적인 사용 사례는 불가능한 경로를 처리하는 것입니다. 예를 들면

simple :: Either Void a -> a
simple (Left x) = absurd x
simple (Right y) = y

이것은 다소 유용한 것이 있습니다. 간단한 유형을 고려하십시오.Pipes

data Pipe a b r
  = Pure r
  | Await (a -> Pipe a b r)
  | Yield !b (Pipe a b r)

이것은 Gabriel Gonzales의 Pipes라이브러리 에서 표준 파이프 유형의 엄격하고 단순화 된 버전입니다 . 이제 우리는 많은 양보하지 않는 파이프 (즉, 소비자)를 다음과 같이 인코딩 할 수 있습니다.

type Consumer a r = Pipe a Void r

이것은 활동적인 양보하지 않습니다. 이것의 의미는 a에 대한 적절한 폴드 규칙 Consumer이

foldConsumer :: (r -> s) -> ((a -> s) -> s) -> Consumer a r -> s
foldConsumer onPure onAwait p 
 = case p of
     Pure x -> onPure x
     Await f -> onAwait $ \x -> foldConsumer onPure onAwait (f x)
     Yield x _ -> absurd x

또는 소비자를 다룰 때 수익률 사례를 무시할 수 있습니다 . 이것이 디자인 패턴의 일반적인 버전입니다. 다형성 데이터 유형을 사용하고 Void필요할 때 가능성을 제거합니다.

아마도 가장 고전적인 용도 Void는 CPS입니다.

type Continuation a = a -> Void

즉, Continuation절대 반환하지 않는 함수입니다. Continuation"not"의 유형 버전입니다. 이것으로부터 우리는 CPS의 모나드를 얻습니다 (고전적인 논리에 해당)

newtype CPS a = Continuation (Continuation a)

Haskell이 순수하기 때문에 우리는이 유형에서 아무것도 얻을 수 없습니다.

---

자유 변수로 매개 변수화 된 람다 항에 대한이 표현을 고려하십시오. (Bellegarde and Hook 1994, Bird and Paterson 1999, Altenkirch and Reus 1999의 논문을 참조하십시오.)

data Tm a  = Var a
           | Tm a :$ Tm a
           | Lam (Tm (Maybe a))

당신은 확실히 건축가라고 Functor이름 Monad을 짓고 대체의 개념을 만들 수 있습니다 .

instance Functor Tm where
  fmap rho (Var a)   = Var (rho a)
  fmap rho (f :$ s)  = fmap rho f :$ fmap rho s
  fmap rho (Lam t)   = Lam (fmap (fmap rho) t)

instance Monad Tm where
  return = Var
  Var a     >>= sig  = sig a
  (f :$ s)  >>= sig  = (f >>= sig) :$ (s >>= sig)
  Lam t     >>= sig  = Lam (t >>= maybe (Var Nothing) (fmap Just . sig))

이제 닫힌 용어를 고려하십시오 . 이들은 Tm Void. 임의의 자유 변수가있는 항에 닫힌 항을 포함해야합니다. 어떻게?

fmap absurd :: Tm Void -> Tm a

물론 아무 작업도하지 않는 용어를 정확히 작업하는 것입니다. 그러나 그것은 unsafeCoerce. 그리고 그것이 vacuous추가 된 이유입니다 Data.Void...

또는 평가하십시오. 다음은 b.

data Val b
  =  b :$$ [Val b]                              -- a stuck application
  |  forall a. LV (a -> Val b) (Tm (Maybe a))   -- we have an incomplete environment

방금 람다를 클로저로 표현했습니다. 평가자는 자유 변수 a를의 값 에 매핑하는 환경에 의해 매개 변수화 b됩니다.

eval :: (a -> Val b) -> Tm a -> Val b
eval g (Var a)   = g a
eval g (f :$ s)  = eval g f $$ eval g s where
  (b :$$ vs)  $$ v  = b :$$ (vs ++ [v])         -- stuck application gets longer
  LV g t      $$ v  = eval (maybe v g) t        -- an applied lambda gets unstuck
eval g (Lam t)   = LV g t

당신은 그것을 짐작했습니다. 모든 대상에서 닫힌 용어를 평가하려면

eval absurd :: Tm Void -> Val b

좀 더 일반적으로 Void는 그 자체로는 거의 사용되지 않지만, 어떤 종류의 불가능 성을 나타내는 방식으로 유형 매개 변수를 인스턴스화하려는 경우에 유용합니다 (예 : 여기서는 닫힌 용어로 자유 변수 사용). 종종 이러한 매개 변수화 된 유형은 매개 변수에 대한 작업을 전체 유형에 대한 작업으로 끌어 올리는 고차 함수와 함께 제공됩니다 (예 : 여기 fmap에서 >>=,, eval). 그래서 당신 absurd은 Void.

또 다른 예를 들어, 사용 상상 Either e v희망이 당신에게 줄 계산 캡처 v하지만 유형의 예외를 일으킬 수를 e. 이 접근 방식을 사용하여 잘못된 동작의 위험을 균일하게 문서화 할 수 있습니다. 완벽하게이 설정에서 계산을 행동 위해 취할 e수 Void, 다음 사용을

either absurd id :: Either Void v -> v

안전하게 달리거나

either absurd Right :: Either Void v -> Either e v

안전하지 않은 세상에 안전한 구성 요소를 포함합니다.

아, 그리고 마지막 만세, "일어날 수 없습니다"를 처리합니다. 커서가있을 수없는 모든 곳에서 일반적인 지퍼 구조로 나타납니다.

class Differentiable f where
  type D f :: * -> *              -- an f with a hole
  plug :: (D f x, x) -> f x       -- plugging a child in the hole

newtype K a     x  = K a          -- no children, just a label
newtype I       x  = I x          -- one child
data (f :+: g)  x  = L (f x)      -- choice
                   | R (g x)
data (f :*: g)  x  = f x :&: g x  -- pairing

instance Differentiable (K a) where
  type D (K a) = K Void           -- no children, so no way to make a hole
  plug (K v, x) = absurd v        -- can't reinvent the label, so deny the hole!

정확히 관련이 없더라도 나머지는 삭제하지 않기로 결정했습니다.

instance Differentiable I where
  type D I = K ()
  plug (K (), x) = I x

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g
  plug (L df, x) = L (plug (df, x))
  plug (R dg, x) = R (plug (dg, x))

instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
  type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
  plug (L (df :&: g), x) = plug (df, x) :&: g
  plug (R (f :&: dg), x) = f :&: plug (dg, x)

실제로 관련성이있을 수 있습니다. 모험심을 느낀다면,이 미완성 기사 에서는 Void자유 변수로 용어 표현을 압축하는 방법을 보여줍니다.

data Term f x = Var x | Con (f (Term f x))   -- the Free monad, yet again

Differentiable및 Traversablefunctor 에서 자유롭게 생성 된 모든 구문 f. 우리가 사용하는 Term f Void여유 변수 영역을 표현하고, [D f (Term f Void)]표현하기 위해 튜브를 고립 자유 변수, 또는 2 개 이상의 자유 변수의 경로의 교차점에 하나 여유 변수 영역을 통해 터널링. 언젠가 그 기사를 끝내야합니다.

값이없는 (또는 적어도 예의 바른 회사에서 말할 가치가없는) 유형의 경우 Void매우 유용합니다. 그리고 absurd그것을 사용하는 방법입니다.

---

"일어날 수없는"경우를 철저히 처리하는 형식 안전 방식으로 어떤 경우에는 유용 ​​할 것이라고 생각합니다.

이것은 정확합니다.

그것은 absurd보다 더 유용하지 않다고 말할 수 const (error "Impossible")있습니다. 그러나 유형이 제한되어 있으므로 유일한 입력 Void은 의도적으로 사람이 살지 않는 데이터 유형 인 유형일 수 있습니다 . 이는 전달할 수있는 실제 값이 없음을 의미합니다 absurd. 유형 검사기가 유형에 대한 액세스 권한이 있다고 생각하는 코드 분기에 도달 Void하면 어리석은 상황에 처한 것입니다. 따라서 absurd기본적으로이 코드 분기에 도달하지 않아야 함을 표시하는 데 사용 합니다.

"Ex falso quodlibet"은 문자 그대로 "[a] false [proposition]에서, 모든 것이 뒤 따른다"를 의미합니다. 따라서 유형이 인 데이터 조각을 보유하고 있음을 발견하면 Void손에 잘못된 증거가 있음을 알 수 있습니다. 당신은 그러므로 채울 수 있는 당신이 (를 통해 원하는 구멍 absurd때문에 거짓 명제에서) 무엇이든은 다음과 같습니다.

나는를 사용하는 예가있는 Conduit의 아이디어에 대한 블로그 게시물을 작성했습니다 absurd.

http://unknownparallel.wordpress.com/2012/07/30/pipes-to-conduits-part-6-leftovers/#running-a-pipeline

---

일반적으로 부분적인 패턴 일치를 방지하는 데 사용할 수 있습니다. 예를 들어, 다음 답변 에서 데이터 유형 선언의 근사치를 잡습니다 .

data RuleSet a            = Known !a | Unknown String
data GoRuleChoices        = Japanese | Chinese
type LinesOfActionChoices = Void
type GoRuleSet            = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices

그런 다음 다음 absurd과 같이 사용할 수 있습니다 .

handleLOARules :: (String -> a) -> LinesOfActionsRuleSet -> a
handleLOARules f r = case r of
    Known   a -> absurd a
    Unknown s -> f s

---

빈 데이터 유형 을 표시 하는 방법에는 여러 가지가 있습니다 . 하나는 빈 대수 데이터 유형입니다. 또 다른 방법은 ∀α.α 또는

type Void' = forall a . a

하스켈에서-이것이 시스템 F에서 인코딩하는 방법입니다 ( 증명 및 유형의 11 장 참조 ). 이 두 가지 설명은 물론 동형이며 동형은 및에서 목격 \x -> x :: (forall a.a) -> Void됩니다 absurd :: Void -> a.

어떤 경우에는 명시 적 변형을 선호합니다. 일반적으로 빈 데이터 유형이 함수의 인수 또는 Data.Conduit 와 같이 더 복잡한 데이터 유형에 나타나는 경우 :

type Sink i m r = Pipe i i Void () m r

어떤 경우에는 다형성 변형을 선호합니다. 일반적으로 빈 데이터 유형은 함수의 반환 유형에 포함됩니다.

absurd 이 두 표현 사이에서 변환 할 때 발생합니다.

---

예를 들어 callcc :: ((a -> m b) -> m a) -> m a(암시 적)을 사용합니다 forall b. ((a -> m Void) -> m a) -> m acontination에 대한 호출이 실제로 반환되지 않으므로 제어를 다른 지점으로 이전하기 때문에 유형일 수도 있습니다 . 연속 작업을하려면 다음을 정의 할 수 있습니다.

type Continuation r a = a -> Cont r Void

(사용할 수는 type Continuation' r a = forall b . a -> Cont r b있지만 랭크 2 유형이 필요합니다.) 그런 다음 vacuousM이 Cont r Void를 Cont r b.

(또한 haskellers.com 을 사용하여 void 패키지를 누가 어떻게 사용하는지 확인하는 것과 같이 특정 패키지의 사용 (역 의존성)을 검색 할 수 있습니다 .)

---

Idris와 같은 종속 유형 언어에서는 Haskell보다 더 유용 할 것입니다. 일반적으로 전체 함수에서 실제로 함수에 넣을 수없는 값과 패턴을 일치시킬 때 무인 유형의 값을 구성 absurd하고 사례 정의를 완료하는 데 사용 합니다.

예를 들어이 함수는 유형 수준의 비용이 포함 된 목록에서 요소를 제거합니다.

shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (x :: ys) Here = ys
shrink (y :: []) (There p) = absurd p
shrink (y :: (x :: xs)) (There p) = y :: shrink (x :: xs) p

두 번째 경우는 빈 목록에 특정 요소가 있다는 말입니다. 그러나 일반적으로 컴파일러는 이것을 알지 못하며 종종 명시 적이어야합니다. 그러면 컴파일러는 함수 정의가 부분적이지 않은지 확인할 수 있으며 더 강력한 컴파일 시간 보장을 얻을 수 있습니다.

Curry-Howard의 관점에서 볼 때, 명제는 어디에 있는지 absurd모순에 의한 증명에서 일종의 QED입니다.

참고 URL : https://stackoverflow.com/questions/14131856/whats-the-absurd-function-in-data-void-useful-for