我使用的是由 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’
有人知道执行此操作的正确方法是什么吗?
最佳答案
我不确定为什么会失败。我同样对实现 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
编译指示,让一切正常工作。
关于haskell - 将 Ord 实例添加到 'singleton' 包生成的自然值,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/39002342/