Lui*_*las 92 haskell type-theory curry-howard
该absurd函数Data.Void具有以下签名,其中,Void是在逻辑上无人居住类型由包导出的:
-- | Since 'Void' values logically don't exist, this witnesses the logical
-- reasoning tool of \"ex falso quodlibet\".
absurd :: Void -> a
我知道足够的逻辑来获得文档的评论,这与命题与类型的对应关系对应于有效的公式? ? a.
令我困惑和好奇的是:这个函数在什么样的实际编程问题上有用？我想也许在某些情况下它可能是一种类型安全的方式来彻底处理"不可能发生"的情况,但我对Curry-Howard的实际用法不太了解,以确定这个想法是否在正确的轨道.
编辑:最好在Haskell中的例子,但如果有人想使用依赖类型的语言我不会抱怨...
pig*_*ker 58
考虑由其自由变量参数化的lambda项的这种表示.(参见Bellegarde和Hook 1994,Bird and Paterson 1999,Altenkirch和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
我刚刚将lambdas表示为闭包.评估器通过将自由变量映射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
在任何从a Differentiable和Traversablefunctor 自由生成的语法中f.我们用Term f Void来表示的区域与没有自由变量,[D f (Term f Void)]以表示管通过的区域,没有自由变量任一的分离的自由变量,或在路径的两个或更多的自由变量的结的隧道.有时必须完成那篇文章.
对于没有价值的类型(或至少,没有值得在礼貌的公司中说话),Void非常有用.你absurd是如何使用它的.
Phi*_* JF 55
生活有点困难,因为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
也就是说,a Continuation是一个永不返回的函数. Continuation是"不"的类型版本.从这里我们得到一个CPS的单子(对应于经典逻辑)
newtype CPS a = Continuation (Continuation a)
由于Haskell是纯粹的,我们无法从这种类型中获得任何东西.
Dan*_*ton 35
我想也许它在某些情况下可能是一种有效处理"不可能发生"案件的类型安全方式
这是完全正确的.
你可以说absurd没有比这更有用了const (error "Impossible").但是,它是类型限制的,因此它的唯一输入可以是某种类型Void,一种故意无人居住的数据类型.这意味着您没有可传递给的实际值absurd.如果你最终在一个代码分支中,类型检查器认为你可以访问某种类型的东西Void,那么,你是在荒谬的情况下.所以你只是absurd用来基本上标记永远不会达到这个代码分支.
"Ex falso quodlibet"字面意思是"来自[a]错误[命题],任何事情都遵循".因此,当您发现自己持有一个类型为的数据时Void,您就会知道手中有错误的证据.因此,你可以填补你想要的任何洞(通过absurd),因为从一个错误的命题,任何事情都随之而来.
我写了一篇关于Conduit背后的想法的博客文章,其中有一个使用的例子absurd.
Dan*_*ner 13
通常,您可以使用它来避免明显部分模式匹配.例如,从此答案中获取数据类型声明的近似值:
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
Pet*_*lák 11
如何表示空数据类型有不同的方法.一种是空代数数据类型.另一种方法是使它成为∀α.α或.的别名
type Void' = forall a . a
在Haskell中 - 这就是我们如何在系统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 a,因为对控制的调用实际上不会返回,它将控制转移到另一个点.如果我们想使用continuation,我们可以定义
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包的人和方式.)