将Ord实例添加到“singleton”包中生成的自然程序

Question

我使用的是非常简单的类型级自然语言，它是用单个程序包生成的。我现在正试图向它们添加一个Ord实例。

{-# LANGUAGE MultiParamTypeClasses, TemplateHaskell, KindSignatures, DataKinds, ScopedTypeVariables, GADTs, TypeFamilies, FlexibleInstances, TypeOperators, UndecidableInstances, InstanceSigs #-}

module Functions where

import Data.Singletons
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Promotion.Prelude

singletons [d|
             data Nat = Z | S Nat
               deriving Eq

             instance Ord Nat where
               (<=)    Z     _  = True
               (<=) (S _)    Z  = False
               (<=) (S n) (S m) = n <= m
             |]

我一直在犯一个又一个错误。最近的一次是：

src/Functions.hs:10:1:
    Couldn't match kind ‘Nat’ with ‘*’
    When matching types
      n0 :: Nat
      t1 :: *
    Expected type: Sing t1
      Actual type: Sing n0
    Relevant bindings include
      n_a9na :: Sing n0 (bound at src/Functions.hs:10:1)
      lambda :: Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10)
        (bound at src/Functions.hs:10:1)
    In the second argument of ‘applySing’, namely ‘n_a9na’
    In the first argument of ‘applySing’, namely
      ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’

src/Functions.hs:10:1:
    Could not deduce (SOrd 'KProxy) arising from a use of ‘%:<=’
    from the context (t00 ~ 'S n)
      bound by a pattern with constructor
                 SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat).
                       (z_a9mg ~ 'S n_a9mh) =>
                       Sing n_a9mh -> Sing z_a9mg,
               in an equation for ‘%:<=’
      at src/Functions.hs:(10,1)-(18,15)
    or from (t10 ~ 'S n1)
      bound by a pattern with constructor
                 SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat).
                       (z_a9mg ~ 'S n_a9mh) =>
                       Sing n_a9mh -> Sing z_a9mg,
               in an equation for ‘%:<=’
      at src/Functions.hs:(10,1)-(18,15)
    or from (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0)
      bound by the type signature for
                 lambda_a9n9 :: (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0) =>
                                Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10)
      at src/Functions.hs:(10,1)-(18,15)
    In the second argument of ‘singFun2’, namely ‘(%:<=)’
    In the first argument of ‘applySing’, namely
      ‘singFun2 (Proxy :: Proxy (:<=$)) (%:<=)’
    In the first argument of ‘applySing’, namely
      ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’

有人知道怎么做才是正确的吗？

Answer 1

我不知道为什么会失败。我同样感到困惑的是，我在实现compare时遇到了类似的失败，更让我困惑的是我在尝试(看似简单的)时遇到的失败。

singletons [d| data Nat = Z | S Nat deriving (Eq,Ord) |]

我猜Ord里有些东西掉了.然而，这是可行的。稍后我会试着看看singleton的内脏。

singletons [d|
              data Nat = Z | S Nat
                 deriving (Eq)

              instance Ord Nat where
                compare = compare'

              compare' :: Nat -> Nat -> Ordering
              compare' Z Z  = EQ
              compare' (S _) Z = GT
              compare' Z (S _) = LT
              compare' (S n) (S m) = compare' n m
             |] 

顺便说一下，我这里用的是GHC8.0。

编辑

在深入研究了singletons之后，我发现了问题的真正根源(并且被类型级别的黑客攻击可能发生的程度所震撼)。使用来自GHC的-ddump-splices，我能够获得实际生成的Haskell代码(用于您问题中的初始代码)。冒犯的部分是

instance PEq (Proxy :: Proxy Nat_a7Vb) where
  type (:==) (a_a8Rs :: Nat_a7Vb) (b_a8Rt :: Nat_a7Vb) = Equals_1627424016_a8Rr a_a8Rs b_a8Rt

和

instance POrd (Proxy :: Proxy Nat_a7Vb) where
  type (:<=) (a_aa9e :: Nat_a7Vb) (a_aa9f :: Nat_a7Vb) = Apply (Apply TFHelper_1627428966Sym0 a_aa9e) a_aa9f

在编译生成的代码时，我收到了对这两种代码都稍微有用的错误消息。

Expecting one more argument to ‘Proxy’
Expected kind ‘Proxy Nat_a7Vb’, but ‘Proxy’ has kind ‘k0 -> *’

用于修饰说明PEq和POrd类中的POrd。如果没有-XPolyKinds，就无法编译。检查singletons的回购，它确实告诉您需要启用-XTypeInType，这反过来又启用了-XPolyKinds。

因此，没有bug，您只需添加PolyKinds或TypeInType (我推荐后者，因为这是包推荐的.)到您的LANGUAGE实用程序，以使一切正常工作。

Answer 2

使用提升的布尔关系是 绝不可能 舒适。布尔人抹去了你对学习感兴趣的信息，当你想要做任何事情的时候，你就会陷入困境。说不就行了孩子们。

还有更好的办法。"n小于或等于m“是一个可以用信息丰富的证据证明的命题。证明一个数字小于另一个数的一种方法是给出它们之间的区别：

data LE n m where
    LE :: Natty z -> LE n (n :+ z)

我们可以想出一个程序来测试一个给定的数字是否小于另一个数字。le试图从m中减去n，然后失败并返回Nothing，或者生成它们之间的差异，作为Natty，并在LE构造函数中打包以证明减法是正确的。

le :: Natty n -> Natty m -> Maybe (LE n m)
le Zy m = Just (LE m)
le (Sy n) (Sy m) = fmap (\(LE z) -> LE z) (le n m)
le _ _ = Nothing

这个想法可以推广到给我们一个“强类型的compare”。当比较两个数字时，你会发现它们是相等的，或者一个比另一个要小。(Either (LE n m) (LE m n)也做了这项工作，但这个版本稍微精确一些。)

data Compare n m where
    LT :: Natty z -> Compare n (n :+ S z)
    EQ :: Compare n n
    GT :: Natty z -> Compare (m :+ S z) m

compare :: Natty n -> Natty m -> Compare n m
compare Zy Zy = EQ
compare Zy (Sy m) = LT m
compare (Sy n) Zy = GT n
compare (Sy n) (Sy m) = case compare n m of
    LT z -> LT z
    EQ -> EQ
    GT z -> GT z

(我是从https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf上提出来的。)

请注意，与le不同，compare是总计的。它总是会给你一个结果:每个数字要么小于，等于，要么大于每一个其他数字。我们的目标是编写一个过程来测试两个数字中哪一个更小，但我们也发现自己证明数字是全序，并编写了一个类型安全的减法例程，所有这些都在同一个函数中。

另一种看待compare的方法是作为对自然数的视图。当你比较两个数字时，你就会知道哪一个比较少，通过多少，你对数字本身的了解就会更加丰富。Agda的点模式对精化的概念有很好的支持：

compare : (n m : Nat) -> Compare n m
compare zero zero = eq
compare zero (suc m) = lt m
compare (suc n) zero = gt n
compare (suc n)            (suc m)           with compare n m
                        -- see how matching on `lt` refines `m` to `n + suc z`
compare (suc n)            (suc .(n + suc z)) | lt z = lt z
compare (suc m)            (suc .m)           | eq = eq
     -- likewise matching on `gt` refines `n` to `m + suc z`
compare (suc .(m + suc z)) (suc m)            | gt z = gt z

无论如何，我不能直接与您的singletons错误的来源交谈，但是Ord很难处理单个值的一个原因是它假设您在比较相同类型的值：

class Ord a where
    compare :: a -> a -> Ordering

当你比较两个单身汉时，他们通常不会有相同的类型！这就是单身人士的全部观点:他们的类型直接反映了他们的价值。如果您有两个Natty n值(它们的n匹配)，那么比较它们就没有多大意义，因为您已经知道它们是相等的；如果它们不相等，就无法比较它们！

非常合理的是，像Ord这样的类是在简单类型的世界中设计的，在依赖类型的程序中不一定那么有用。如果您使用的是依赖类型，那么正确的方法就是不要滥用旧的工具。迎来这个安全、信息丰富的新世界，张开双臂进行编程！