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

자유 변수로 매개 변수화 된 람다 항에 대한이 표현을 고려하십시오. (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.NET에서 범용 작업으로 전달 Void합니다.

또 다른 예를 들어,를 사용하여 Either e v를 제공 v하지만 type 예외를 발생시킬 수있는 계산을 캡처하는 데 사용한다고 상상해보십시오 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그것을 사용하는 방법입니다.