如何解构SNat（单身人士） [英] How to deconstruct an SNat (singletons)
问题描述
我正在Haskell中试验依赖类型，并在 paper ：
replicate2 :: forall n a。 SingI n => a - > Vec a n
replicate2 a = case（sing :: Sing n）of
SZero - > VNil
SSucc _ - > VCons a（replicate2 a）
所以我试图自己实现这一点，只是想知道它是如何作品：
{ - ＃LANGUAGE DataKinds＃ - }
{ - ＃LANGUAGE GADTs＃ - }
{ - ＃LANGUAGE KindSignatures＃ - }
{ - ＃LANGUAGE TypeOperators＃ - }
{ - ＃LANGUAGE RankNTypes＃ - }
{ - ＃LANGUAGE ScopedTypeVariables＃ - }
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
data V :: Nat - > * - > *其中
无:: V 0 a
（：>）:: a - > V n a - > V（n：+ 1）a
infixr 5：>
replicateV :: SingI n => a - > V n a
replicateV = replicateV'sing
where replicateV':: Sing n - > a - > V n a
replicateV'sn a =
的情况sn SNat - >未定义 - 我可以用这个做什么？
现在问题在于 Sing 实例对于 Nat 没有 SZero 或 SSucc 。只有一个构造函数叫做 SNat 。
> ：info Sing
数据实例Sing n其中
SNat :: KnownNat n => Sing n
这与其他允许匹配的单例不同，比如 STrue 和 SFalse ，例如以下（无用）示例：
data Foo :: Bool - > * - > *其中
T :: a - > Foo True a
F :: a - > Foo False a
foo :: forall a b。 SingI b => a - > Foo b a
foo a = case（sing :: Sing b）of
STrue - > T a
SFalse - > F a
您可以使用 fromSing 来获取一个基本类型，但是这当然确实允许GHC检查输出向量的类型：
- 不会检测
replicateV2 :: SingI n => a - > V n a
replicateV2 = replicateV'sing
where replicateV':: Sing n - > a - > V n a
replicateV'sn a =来自
0的Sn的情况 - >>无
n - > a：> replicateV2 a
所以我的问题是：如何实现 erisco给出的答案解释了为什么我的方法解构 但是，这似乎并没有给编译器提供足够的信息来推断 这会产生以下错误： 所以，我原来的问题仍然存在，我仍然无法对 从评论中，我担心我一定会错过一些非常明显的东西，但这是我的承诺。整点： 是，为了返回 现在 当然，还有另一种方法来专门化一个返回 replicateV
$ b SNat 不起作用。但即使使用 type-natural 库，我也无法为 V实现 replicateV 数据类型使用GHC的内置 Nat 类型。
<例如下面的代码编译：
replicateV :: SingI n => a - > V n a
replicateV = replicateV'sing
where replicateV':: Sing n - > a - > V n a
replicateV'sn a =案例TN.sToPeano sn
TN.SZ - > undefined
（TN.SS sn'） - > undefined
n 是 0 或不是。例如，以下给出了一个编译器错误：
replicateV :: SingI n => a - > V n a
replicateV = replicateV'sing
where replicateV':: Sing n - > a - > V n a
replicateV'sn a =案例TN.sToPeano sn
TN.SZ - >无
（TN.SS sn'） - > undefined
src / Vec.hs：25：28：error：
•无法从上下文推导出：n1〜0
：TN.ToPeano n1〜'TN。 Z
由构造函数的模式绑定：
TN.SZ :: forall（z0 :: TN.Nat）。 z0〜'TN.Z =>在src / Vec.hs：25：13-17替代
的情况下使用z0，
'n1'是一个刚性类型变量，由
绑定，类型签名用于：
replicateV':: forall（n1 :: Nat）a1。 Sing n1 - > a1 - > V n1 a1
at src / Vec.hs：23：24
预期类型：V n1 a1
实际类型：V 0 a1
•在表达式中：Nil
在另一种情况下：TN.SZ - >无
在表达式中：
case {
TN.SZ的TN.sToPeano sn>无
（TN.SS sn'） - > undefined}
•相关绑定包括
sn :: Sing n1（绑定在src / Vec.hs：24：21）
replicateV':: Sing n1 - > a1 - > V n1 a1（绑定在src / Vec.hs：24：9）
SNat 做任何有用的事情。
replicate2 :: forall n a。 SingI n => a - > Vec a n
replicate2 a = case（sing :: Sing n）of
SZero - > VNil
SSucc _ - > VCons a（replicate2 a）
VNil： ：当函数具有常规返回类型，您需要专门化 Vec an 时，Vec a 0 n 到 0 ，并且GADT上的模式匹配为您提供了一种方法，只要您有一个构造函数，如 SZero code>，这意味着 n〜0 。
SNat s在单例包中没有这样的构造函数。就我所知，获得一个唯一的方法是为自然构建一个全新的单体类型并实现必要的类型族。也许你可以用包装 Nat s的方式来做，所以你更接近 SZero :: Sing（SN 0）， SNonZero :: Sing（SN n）比一个Peano建筑，但我不知道。
Vec an 的函数来返回 Vec a 0 ，即如果你愿意放弃一些显式的单例机制并切换到类型类（并且还允许重叠和不可判定的实例），以下内容似乎起作用。我必须稍微修改 V 的定义，以使用 n： - 1 而不是 n ：+ 1 ，但我不认为 存在问题。
<$ c $ b $ {$＃$} { - ＃LANGUAGE DataKinds＃ - }
{ - ＃LANGUAGE GADTs＃ - }
{ - ＃LANGUAGE KindSignatures＃ - }
{ - ＃LANGUAGE TypeOperators＃ - }
$ - $ L $ $ $ $ $ { - ＃LANGUAGE RankNTypes＃ - }
{ - ＃LANGUAGE ScopedTypeVariables＃ - }
{ - ＃LANGUAGE FlexibleInstances＃ - }
{ - ＃LANGUAGE FlexibleContexts＃ - }
{ - ＃LANGUAGE OverlappingInstances＃ - }
{ - ＃LANGUAGE UndecidableInstances＃ - }
导入Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
data V :: Nat - > * - > *其中
无:: V 0 a
（：>）:: a - > V（n：-1）a - > V n a
infixr 5：>
class VC n a where
replicateV :: a - > V n a
实例VC 0 a其中
replicateV _ =无
实例VC（n： - 1）a => VC n a其中
replicateV x = x：> replicateV x
instance（显示a）=> Show（V na）where
show Nil =Nil
show（x：> v）= show x ++：>++ show v
headV :: V（n：+ 1）a - > a
headV（x：> _）= x
tailV ::（（n：+ 1）： - 1）〜n => V（n：+ 1）a - > V
tailV（_：> v）= v
main = do print（replicateV False :: V 0 Bool）
print（replicateV 1 :: V 1 Int ）
print（replicateVThree:: V 3 String）
I am experimenting with depedent types in Haskell and came across the following in the paper of the 'singletons' package:
replicate2 :: forall n a. SingI n => a -> Vec a n
replicate2 a = case (sing :: Sing n) of
SZero -> VNil
SSucc _ -> VCons a (replicate2 a)
So I tried to implement this myself, just toget a feel of how it works:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
data V :: Nat -> * -> * where
Nil :: V 0 a
(:>) :: a -> V n a -> V (n :+ 1) a
infixr 5 :>
replicateV :: SingI n => a -> V n a
replicateV = replicateV' sing
where replicateV' :: Sing n -> a -> V n a
replicateV' sn a = case sn of
SNat -> undefined -- what can I do with this?
Now the problem is that the Sing instance for Nat does not have SZero or SSucc. There is only one constructor called SNat.
> :info Sing
data instance Sing n where
SNat :: KnownNat n => Sing n
This is different than other singletons that allow matching, such as STrue and SFalse, such as in the following (useless) example:
data Foo :: Bool -> * -> * where
T :: a -> Foo True a
F :: a -> Foo False a
foo :: forall a b. SingI b => a -> Foo b a
foo a = case (sing :: Sing b) of
STrue -> T a
SFalse -> F a
You can use fromSing to get a base type, but this of course does allow GHC to check the type of the output vector:
-- does not typecheck
replicateV2 :: SingI n => a -> V n a
replicateV2 = replicateV' sing
where replicateV' :: Sing n -> a -> V n a
replicateV' sn a = case fromSing sn of
0 -> Nil
n -> a :> replicateV2 a
So my question: how to implement replicateV?
EDIT
The answer given by erisco explains why my approach of deconstructing an SNat does not work. But even with the type-natural library, I am unable to implement replicateV for the V data type using GHC's build-in Nat types.
For example the following code compiles:
replicateV :: SingI n => a -> V n a
replicateV = replicateV' sing
where replicateV' :: Sing n -> a -> V n a
replicateV' sn a = case TN.sToPeano sn of
TN.SZ -> undefined
(TN.SS sn') -> undefined
But this does not seem to give enough information to the compiler to infer whether n is 0 or not. For example the following gives a compiler error:
replicateV :: SingI n => a -> V n a
replicateV = replicateV' sing
where replicateV' :: Sing n -> a -> V n a
replicateV' sn a = case TN.sToPeano sn of
TN.SZ -> Nil
(TN.SS sn') -> undefined
This gives the following error:
src/Vec.hs:25:28: error:
• Could not deduce: n1 ~ 0
from the context: TN.ToPeano n1 ~ 'TN.Z
bound by a pattern with constructor:
TN.SZ :: forall (z0 :: TN.Nat). z0 ~ 'TN.Z => Sing z0,
in a case alternative
at src/Vec.hs:25:13-17
‘n1’ is a rigid type variable bound by
the type signature for:
replicateV' :: forall (n1 :: Nat) a1. Sing n1 -> a1 -> V n1 a1
at src/Vec.hs:23:24
Expected type: V n1 a1
Actual type: V 0 a1
• In the expression: Nil
In a case alternative: TN.SZ -> Nil
In the expression:
case TN.sToPeano sn of {
TN.SZ -> Nil
(TN.SS sn') -> undefined }
• Relevant bindings include
sn :: Sing n1 (bound at src/Vec.hs:24:21)
replicateV' :: Sing n1 -> a1 -> V n1 a1 (bound at src/Vec.hs:24:9)
So, my original problem still remains, I am still unable to do anything usefull with the SNat.
From the comments, I'm worried I must be missing something terrifically obvious, but here's my take on it. The whole point of:
replicate2 :: forall n a. SingI n => a -> Vec a n
replicate2 a = case (sing :: Sing n) of
SZero -> VNil
SSucc _ -> VCons a (replicate2 a)
is that, in order to return VNil :: Vec a 0 when the function has general return type Vec a n, you need to specialize the n to 0, and pattern-matching on GADTs provides a way to do this, as long as you have a constructor, like SZero, that implies n ~ 0.
Now the SNats in the singleton package have no such constructor. The only way to get one, as far as I can see, is to build a whole new singleton type for naturals and implement the necessary type families. Maybe you can do it in a way that wraps the Nats, so you're closer to SZero :: Sing (SN 0), SNonZero :: Sing (SN n) than a Peano construction, but I don't know.
Of course, there's another way to specialize a function that returns Vec a n to return Vec a 0, namely type classes.
If you are willing to abandon some of the explicit singleton machinery and switch to type classes (and also allow overlapping and undecidable instances), the following seems to work. I had to slightly modify the definition of V to use n :- 1 instead of n :+ 1, but I don't think that poses a problem.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
data V :: Nat -> * -> * where
Nil :: V 0 a
(:>) :: a -> V (n :- 1) a -> V n a
infixr 5 :>
class VC n a where
replicateV :: a -> V n a
instance VC 0 a where
replicateV _ = Nil
instance VC (n :- 1) a => VC n a where
replicateV x = x :> replicateV x
instance (Show a) => Show (V n a) where
show Nil = "Nil"
show (x :> v) = show x ++ " :> " ++ show v
headV :: V (n :+ 1) a -> a
headV (x :> _) = x
tailV :: ((n :+ 1) :- 1) ~ n => V (n :+ 1) a -> V n a
tailV (_ :> v) = v
main = do print (replicateV False :: V 0 Bool)
print (replicateV 1 :: V 1 Int)
print (replicateV "Three" :: V 3 String)
这篇关于如何解构SNat（单身人士）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
