Hask或Agda有均衡器吗？

Question

关于这是一个数学问题还是一个问题,我有点犹豫不决,但我怀疑数学家一般不太可能不太了解或关心这个类别,而Haskell程序员可能会这么做.

因此,我们知道Hask或多或少都有产品(当然,我正在使用idealized-Hask).我对它是否有均衡器感兴趣(在这种情况下它将具有所有有限的限制).

直观地看起来并不是这样,因为你不能像套装一样进行分离,因此一般来说,子对象看起来很难构建.但是对于你想要提出的任何特定情况,似乎你可以通过在Set中计算均衡器并计算它来破解它(因为毕竟,每个Haskell类型都是可数的,并且每个可数集都是同形或者是有限类型,也可以是自然类,Haskell都有.所以我看不出我是如何寻找反例的.

现在,阿格达似乎更有前途一点:那里是比较容易形成子对象.显而易见的sigma类型? A (? x ? f x == g x)是均衡器吗？如果细节不起作用,它在道德上是均衡器吗？

Answer 1

提议的候选人不是一个平衡者,但其无关紧要的对手是

Agda中均衡器的候选者看起来很好.所以我们试试吧.我们需要一些基本套件.这是我的refusenik ASCII依赖对类型和均匀的内涵相等.

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg

data _==_ {X : Set}(x : X) : X -> Set where
  refl : x == x

这是两个函数均衡器的候选者

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Sg S \ s -> f s == g s

与fst投影发送Q f g到S.

它说的是:元素Q f g是s源类型的元素,以及证据f s == g s.但这是均衡器吗？让我们试着这样做.

要说均衡器是什么,我应该定义功能组合.

_o_ : {R S T : Set} -> (S -> T) -> (R -> S) -> R -> T
(f o g) x = f (g x)

所以现在我需要证明任何h : R -> S识别f o h并且g o h必须通过候选人考虑的因素fst : Q f g -> S.我需要提供其他组件,u : R -> Q f g以及确实h因素的证据fst o u.这是图片:(Q f g , fst)是一个均衡器,如果图表没有通勤u,有一种独特的方式来添加u图表仍然通勤.

这里有调解的存在u.

mediator : {R S T : Set}(f g : S -> T)(h : R -> S) ->
           (q : (f o h) == (g o h)) ->
           Sg (R -> Q f g) \ u -> h == (fst o u)

很显然,我应该选择同一元素的S那个h选秀权.

mediator f g h q = (\ r -> (h r , ?0)) , ?1

给我两个证明义务

?0 : f (h r) == g (h r)
?1 : h == (\ r -> h r)

现在,?1可以refl像Agda的定义平等一样具有函数的eta定律.因为?0,我们很幸运q.平等功能尊重应用

funq : {S T : Set}{f g : S -> T} -> f == g -> (s : S) -> f s == g s
funq refl s = refl

所以我们可以采取?0 = funq q r.

但是,让我们不要过早地庆祝,因为调解态射的存在是不够的.我们还需要它的独特性.在这里,轮子可能会变得不稳定,因为它==是内在的,所以唯一性意味着只有一种方法来实现中介地图.但是,我们的假设也是强烈的......

这是我们的证明义务.我们必须证明任何其他中介态射等于所选择的态度mediator.

mediatorUnique :
  {R S T : Set}(f g : S -> T)(h : R -> S) ->
  (qh : (f o h) == (g o h)) ->
  (m : R -> Q f g) ->
  (qm : h == (fst o m)) ->
  m == fst (mediator f g h qh)

我们可以立即替换qm并获得

mediatorUnique f g .(fst o m) qh m refl = ?

? :  m == (\ r -> (fst (m r) , funq qh r))

看起来不错,因为Agda有记录的eta法则,所以我们知道

m == (\ r -> (fst (m r) , snd (m r)))

但是当我们尝试制作时? = refl,我们会收到投诉

snd (m _) != funq qh _ of type f (fst (m _)) == g (fst (m _))

这很烦人,因为身份证明是唯一的(在标准配置中).现在,您可以通过假设扩展性和使用其他一些关于相等性的事实来摆脱这种局面

postulate ext : {S T : Set}{f g : S -> T} -> ((s : S) -> f s == g s) -> f == g

sndq : {S : Set}{T : S -> Set}{s : S}{t t' : T s} ->
       t == t' -> _==_ {Sg S T} (s , t) (s , t')
sndq refl = refl

uip : {X : Set}{x y : X}{q q' : x == y} -> q == q'
uip {q = refl}{q' = refl} = refl

? = ext (\ s -> sndq uip)

但这太过分了,因为唯一的问题是令人讨厌的等式证明不匹配:实现的可计算部分匹配在鼻子上.所以解决方法是无关紧要.余取代Sg由Existential量词,其第二组件被标记为与不相关的点.现在重要的不是我们使用哪种证据证明证人是善的.

record Ex (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    .snd : T fst
open Ex

而新的候选均衡器是

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Ex S \ s -> f s == g s

除了最后的义务之外,整个建筑都和以前一样

? = refl

被接受了!

所以是的,即使在内涵设置中,eta定律和将字段标记为无关的能力也会给我们带来均衡.

在这种结构中没有涉及不可判断的类型检查.

Answer 2

Hask

Hask没有均衡器.需要记住的一件重要事情是,考虑类型(或任何类别中的对象)及其同构类确实需要考虑箭头.你对底层集的看法是正确的,但具有同构底层集的类型肯定不一定是同构的.Hask和Set之间的一个区别是Hask的箭头必须是可计算的,事实上对于理想化的Hask,它们必须是完全的.

我花了一些时间试图想出一个真实可辩护的反例,并发现一些参考文献暗示它无法完成,但没有证据.但是,如果你愿意的话,我确实有一些"道德的"反例.我无法证明Haskell中不存在均衡器,但它似乎无法实现!

例1

f, g: ([Int], Int) -> Int

f (p,v) = treat p as a polynomial with given coefficients, and evaluate p(v).
g _ = 0

均衡器"应该"是p(n)= 0的所有对(p,n)的类型,以及将这些对注入([Int],Int)的函数.根据希尔伯特的第10个问题,这个集合是不可判定的.在我看来,这应该排除它是Haskell类型的可能性,但我不能证明(有可能有一些奇怪的方法构建这种类型,没有人发现？).也许我没有连接一两个点 - 也许证明这是不可能的并不难？

例2

假设您有编程语言.您有一个编译器,它接受源代码和输入并生成一个函数,函数的固定点是输出.(虽然我们没有像这样的编译器,但是指定类似的语义并不是闻所未闻的).所以你有了

compiler : String -> Int -> (Int -> Int)

(联合国)把它变成一个功能

compiler' : (String, Int, Int) -> Int

并添加一个功能

id' : (String, Int, Int) -> Int
id' (_,_,x) = x

然后编译器',id'的均衡器将是源程序,输入,输出的三元组的集合 - 这是不可计算的,因为编程语言是完全通用的.

更多例子

选择你最喜欢的不可判定的问题:它通常涉及决定某个对象是否是某个集合的成员.您通常具有可用于检查特定对象的此属性的总函数.您可以使用此函数创建均衡器,其中类型应该是不可判定集中的所有项目.这就是前两个例子的来源,还有更​​多.

阿格达

我对Agda并不熟悉.我的直觉是你的sigma类型应该是一个均衡器:你可以写下类型,以及必要的注入函数,它看起来完全满足定义.但是,作为不使用Agda的人,我认为我没有资格查看详细信息.

但真正的实际问题是,sigma类型的类型检查并不总是可计算的,所以这样做并不总是有用的.在上面的所有示例中,您可以记下您提供的Sigma类型,但如果没有证据,您将无法轻易检查某些内容是否属于该类型的成员.

顺便说一句,这就是为什么Haskell不应该有均衡器的原因:如果确实如此,那么类型检查将是不可判定的!依赖类型使得一切都变得简单.他们应该能够在其类型中表达有趣的数学结构,而Haskell则不能,因为它的类型系统是可以决定的.因此,我自然希望理想化的Agda具有所有有限的限制(否则我会感到失望).其他依赖类型的语言也是如此; 例如,Coq肯定应该有所有限制.