将Ord实例添加到'singleton'包生成的自然对象 [英] Adding an Ord instance to 'singleton' package generated naturals
问题描述
我正在使用由singletons包生成的非常简单的类型级自然。
$ b
{ - ＃LANGUAGE MultiParamTypeClasses，TemplateHaskell，KindSignatures，DataKinds，ScopedTypeVariables， GADTs，TypeFamilies，FlexibleInstances，TypeOperators，UndecidableInstances，InstanceSigs＃ - }
模块函数其中
导入Data.Singletons
导入Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Promotion.Prelude
singletons [d |
数据Nat = Z | S Nat
导出Eq
实例Ord Nat其中
（<=）Z_ = True
（<=）（S _）Z = False
（<=）（S n）（S m）= n <= m
|]
我一次接连发生一次错误。最新的是：
src / Functions.hs：10：1：
无法匹配kind'Nat 'with'*'
当匹配类型
n0 :: Nat
t1 :: *
预期类型：Sing t1
实际类型：Sing n0
相关绑定包括
n_a9na :: Sing n0（绑定在src / Functions.hs：10：1）
lambda :: Sing n0 - > Sing m0 - >
（在src / Functions.hs：10：1处绑定）
在'applySing'的第二个参数中，即'n_a9na'（应用（应用（：<= $）t00）t10）
在'applySing'的第一个参数中，即
'applySing（singFun2（Proxy :: Proxy（：<= $））（％：<=））n_a9na'
src / Functions.hs：10：1：
由于使用上下文中的'％：<='
导致无法推断（SOrd'KProxy）（t00〜'S n ）
由具有构造函数
SS :: forall（z_a9mg :: Nat）（n_a9mh :: Nat）的模式绑定。
（z_a9mg〜'S n_a9mh）=>
Sing n_a9mh - >在src / Functions.hs：（10,1） - （18,15）
或来自（t10〜'）的'％：<='
的等式中Sing z_a9mg，
， S n1）
由构造函数
SS :: forall（z_a9mg :: Nat）（n_a9mh :: Nat）绑定。
（z_a9mg〜'S n_a9mh）=>
Sing n_a9mh - >在src / Functions.hs：（10,1） - （18,15）
或from（t00〜Apply）中为'％：<='
的等式中创建z_a9mg，
对于
lambda_a9n9 ::（t00〜Apply SSym0 n0，t10〜Apply SSym0 m0）=>的情况，由类型签名限制的SSym0 n0，t10〜Apply SSym0 m0）
Sing n0 - > Sing m0 - >在src / Functions.hs中应用（应用（应用（：<= $）t00）t10）
：（10,1） - （18,15）
在'singFun2'的第二个参数中，在'applySing'的第一个参数中，即
'singFun2（Proxy :: Proxy（：<= $））（％：<= $） ）'
'applySing'的第一个参数，即
'applySing（singFun2（Proxy :: Proxy（：<= $））（％：<=））n_a9na'
有没有人知道做这件事的正确方法是什么？
我不知道为什么这是失败的。我对执行比较时遇到的类似失败同样感到困惑，而对于尝试（看似简单）
$ b
singletons [d |数据Nat = Z | S Nat推导（Eq，Ord）|]
我的猜测是 Ord 已关闭...但是，这起作用。稍后我会试着看看 singleton 的内涵。
singletons [d |
数据Nat = Z | S Nat
deriving（Eq）
instance Ord Nat where
compare = compare'
compare':: Nat - > Nat - > （S _）= LT
比较'（S n）（S m） = compare'nm
|]
顺便说一句，我在这里使用GHC 8.0 。
编辑
在 singletons ，我发现了问题的真正根源（并且已经被多少类型级的hackery所淹没）。使用来自GHC的 -ddump-splices 我能够获得生成的实际Haskell代码（用于问题中的初始代码）。有问题的部分是
pre $实例PEq（Proxy :: Proxy Nat_a7Vb）其中
类型（：==）（a_a8Rs :: Nat_a7Vb）（b_a8Rt :: Nat_a7Vb）= Equals_1627424016_a8Rr a_a8Rs b_a8Rt
和
instance POrd（Proxy :: Proxy Nat_a7Vb）其中
类型（：<=）（a_aa9e :: Nat_a7Vb）（a_aa9f :: Nat_a7Vb ）= Apply（应用TFHelper_1627428966Sym0 a_aa9e）a_aa9f
编译生成的代码后，我收到了稍微有用的错误这两个消息的消息
期待'Proxy'的另外一个参数
期望种类'Proxy Nat_a7Vb'，但'代理'有种'k0 - > *'
属于（Proxy :: Proxy Nat_a7Vb） PEq 和 POrd 类。如果没有 -XPolyKinds 。检查了 singletons 的回购，事实上它告诉你需要 -XTypeInType 启用，这又启用<$ c
因此，没有错误，您只需添加 PolyKinds code>或 TypeInType （我推荐后者，因为这是包的建议......）到 LANGUAGE 编译指示让所有的东西都起作用。
I am using very simple type-level naturals generated with the singletons package. I am now trying to add an Ord instance to them.
{-# 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
|]
I have been hitting one error after the other. The latest one is:
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’
Does anyone have an idea what the correct way to do this is?
I'm not sure why this is failing. I am equally puzzled by a similar failure I get when implementing compare instead, and even more puzzled by the failure I get when trying the (seemingly simple)
singletons [d| data Nat = Z | S Nat deriving (Eq,Ord) |]
My guess is that something in Ord is off... However, this works. I'm gonna try to take a look at the guts of singleton later.
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
|]
By the way, I'm using GHC 8.0 here.
EDIT
After poking around in singletons, I've found the real source of problems (and been blown away with how much type-level hackery is possible). Using -ddump-splices from GHC I was able to get the actual Haskell code generated (for the initial code in your question). The offending parts were
instance PEq (Proxy :: Proxy Nat_a7Vb) where
type (:==) (a_a8Rs :: Nat_a7Vb) (b_a8Rt :: Nat_a7Vb) = Equals_1627424016_a8Rr a_a8Rs b_a8Rt
and
instance POrd (Proxy :: Proxy Nat_a7Vb) where
type (:<=) (a_aa9e :: Nat_a7Vb) (a_aa9f :: Nat_a7Vb) = Apply (Apply TFHelper_1627428966Sym0 a_aa9e) a_aa9f
Compiling the code generated, I received the slightly more useful error message for both of these
Expecting one more argument to ‘Proxy’
Expected kind ‘Proxy Nat_a7Vb’, but ‘Proxy’ has kind ‘k0 -> *’
pertaining to the (Proxy :: Proxy Nat_a7Vb) in the PEq and POrd classes. That won't compile without -XPolyKinds. Checked the repo for singletons and indeed it tells you that you need -XTypeInType enabled, which in turn enables -XPolyKinds.
So, there is no bug, you just need to add either PolyKinds or TypeInType (I recommend the latter, since that is what the package recommends...) to your LANGUAGE pragmas to get everything to work.
这篇关于将Ord实例添加到'singleton'包生成的自然对象的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
