GADT可以用来证明GHC中的类型不等式吗？ [英] Can GADTs be used to prove type inequalities in GHC?

问题描述

因此，在我一直试图通过小哈斯克尔练习来理解库里霍华德的过程中，我一直在坚持：

  { - ＃LANGUAGE GADTs＃ - } 
 
 import Data.Void 
 
 type Not a = a  - >无效
 
  -  |类型相等证明的类型，只有在a = b时才能被实例化。 
数据等于b其中
 Refl ::等于a 
 
  -  |从@Equal Int Char @推定的证明推导出一个矛盾。 
 intIsNotChar :: Not（Equal Int Char）
 intIsNotChar intIsChar = ??? 
  

很明显，类型 Equal Int Char 没有（非底部）居民，因此在语义上应该是 absurdEquality :: Equal Int Char - >一个函数......但是对于我来说，我无法找出任何方法来写一个比使用 undefined 的方法。

所以：

1. 我缺少一些东西，或者


2. 语言的某些限制使得这是不可能完成的任务，我还没有设法理解它是什么。

我怀疑答案是这样的：编译器无法利用这个事实，即没有 Equal 构造函数没有a = b。但是如果是这样的话，是什么使它成真？

解决方案

这是Philip JF解决方案的缩写版本，类型理论家多年来一直在反驳方程式。

 类型家庭判别式x 
类型实例判别式Int =（）
 type instance Discriminate Char = Void 
 
 transport :: Equal ab  - >区分 - >区分b 
运输Refl d = d 
 
反驳:: Equal Int Char  - >无效
反驳q =运输q（）
  

为了表明事情的不同，你必须通过提供一个计算上下文来捕捉它们的行为，以产生不同的观察结果。 Discriminate 正好提供了这样一种上下文：一种类型级别的程序，它以不同的方式处理这两种类型。

它不是需要诉诸 undefined 来解决这个问题。总编程有时会涉及拒绝不可能的输入。即使在 undefined 可用的情况下，我建议不要在总方法满足的地方使用它：总方法解释为什么某些事情是不可能的，而typechecker证实; 未定义仅仅是文件您的承诺。事实上，这种驳斥的方式是Epigram在确保案例分析涵盖其领域的同时，不再需要不可能的案例。至于计算行为，请注意 refute ，通过 transport 在 q 中必然是严格的，而 q 无法计算为在空上下文中正常形式的头，因为没有这样的头标准形式存在（并且因为计算保留了类型，当然）。在总体设置中，我们确信在运行时永远不会调用 refute 。在Haskell中，我们至少可以确定，在我们必须回应它之前，它的论点会发生分歧或抛出异常。一个 lazy 版本，比如

  absurdEquality e =错误您有一个类型错误可能导致大问题
  

会忽略 e 并告诉你，如果没有，则会出现类型错误。我更喜欢

  absurdEquality e = e`seq`错误如果发生这种情况，请告诉我
  

如果诚实的反驳太过于辛苦。

So, in my ongoing attempts to half-understand Curry-Howard through small Haskell exercises, I've gotten stuck at this point:

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

Clearly the type Equal Int Char has no (non-bottom) inhabitants, and thus semantically there ought to be an absurdEquality :: Equal Int Char -> a function... but for the life of me I can't figure out any way to write one other than using undefined.

So either:

1. I'm missing something, or
2. There is some limitation of the language that makes this an impossible task, and I haven't managed to understand what it is.

I suspect the answer is something like this: the compiler is unable to exploit the fact that there are no Equal constructors that don't have a = b. But if that is so, what makes it true?

解决方案

Here's a shorter version of Philip JF's solution, which is the way dependent type theorists have been refuting equations for years.

type family Discriminate x
type instance Discriminate Int  = ()
type instance Discriminate Char = Void

transport :: Equal a b -> Discriminate a -> Discriminate b
transport Refl d = d

refute :: Equal Int Char -> Void
refute q = transport q ()

In order to show that things are different, you have to catch them behaving differently by providing a computational context which results in distinct observations. Discriminate provides exactly such a context: a type-level program which treats the two types differently.

It is not necessary to resort to undefined to solve this problem. Total programming sometimes involves rejecting impossible inputs. Even where undefined is available, I would recommend not using it where a total method suffices: the total method explains why something is impossible and the typechecker confirms; undefined merely documents your promise. Indeed, this method of refutation is how Epigram dispenses with "impossible cases" whilst ensuring that a case analysis covers its domain.

As for computational behaviour, note that refute, via transport is necessarily strict in q and that q cannot compute to head normal form in the empty context, simply because no such head normal form exists (and because computation preserves type, of course). In a total setting, we'd be sure that refute would never be invoked at run time. In Haskell, we're at least certain that its argument will diverge or throw an exception before we're obliged to respond to it. A lazy version, such as

absurdEquality e = error "you have a type error likely to cause big problems"

will ignore the toxicity of e and tell you that you have a type error when you don't. I prefer

absurdEquality e = e `seq` error "sue me if this happens"

if the honest refutation is too much like hard work.

这篇关于GADT可以用来证明GHC中的类型不等式吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！