haskell - 将 Ord 实例添加到 'singleton' 包生成的自然值

Question

我使用的是由 singletons 包生成的非常简单的类型级自然数。我现在正在尝试向其中添加一个 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
             |] 

顺便说一下，我这里使用的是 GHC 8.0。

编辑

在研究了单例之后，我发现了问题的真正根源(并且对类型级黑客攻击的可能性感到震惊)。使用 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 类中的 (Proxy::Proxy Nat_a7Vb) 有关。如果没有 -XPolyKinds 则无法编译。检查了 singletons 的存储库，确实它告诉您需要启用 -XTypeInType，从而启用 -XPolyKinds。

所以，没有错误，您只需要添加 PolyKinds 或 TypeInType (我推荐后者，因为这是软件包推荐的......)到您的 LANGUAGE 编译指示，让一切正常工作。