我正在 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 -> * -> * 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?
现在的问题是Sing
实例为Nat
不具有SZero
or SSucc
。只有一个构造函数称为SNat
.
> :info Sing
data instance Sing n where
SNat :: KnownNat n => Sing n
这与其他允许匹配的单例不同,例如STrue
and SFalse
,例如下面的(无用的)示例:
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
您可以使用fromSing
获取基本类型,但这当然允许 GHC 检查输出向量的类型:
-- 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
所以我的问题是:如何实施replicateV
?
EDIT
erisco 给出的答案解释了为什么我解构一个SNat
不起作用。但即使有type-natural
图书馆,我无法实施replicateV
为了V
数据类型使用GHC的内置Nat
types.
例如下面的代码可以编译:
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
但这似乎没有为编译器提供足够的信息来推断是否n
is 0
或不。例如,以下给出了编译器错误:
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
这会产生以下错误:
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)
所以,我原来的问题仍然存在,我仍然无法做任何有用的事情SNat
.