如何解构SNAT（单身）

问题描述：

我在哈斯克尔depedent类型的试验，并在“单身”包的paper遇到下列传来：如何解构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)

于是，我就这样实现我自己，只是toget它是如何工作的感觉：

{-# 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或SSucc。只有一个名为SNat的构造函数。

> :info Sing 
data instance Sing n where 
    SNat :: KnownNat n => Sing n

这比其它的单身，其允许匹配，如STrue和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？

编辑

通过erisco给出的答案解释了为什么我的解构的SNat方法是行不通的。但即使对于type-natural库，我也无法实现replicateV的V数据类型使用GHC的内置Nat类型。

例如，下面的代码编译：

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是否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。

这带出了我讨厌GHC内建的'Nat'类型的一切。证明'（n + 1） - 1〜n'等事情的不可能性，以及检查'n〜0'的尴尬。 'replicateV2'是一个基本的递归操作，你需要在矢量长度上进行归纳。没有对“纳特”的归纳定义，你无处可去。让我明确地说：任何解决问题的方法都会使用绕过类型系统的东西（通过插件或unsafeCoerce）。另一方面，你可以用'数据Nat = Z |安全而又轻松地完成任何事情S Nat'。 – Alec

这就是我开始害怕的事情，实际上没有解决这个问题的方法。但我希望有一些我不知道的常用解决方法。我会等待，直到赏金结束希望奇迹。但是，如果没有，那么我想你的评论回答我的问题，我会诉诸使用'unsafeCoerce'。 –

我非常热衷于使用内置'Nat'的原因是我使用的一些库也使用内置的'Nat'类型。特别是来自'hmatrix'的'Numeric.LinearAlgebra.Static'。在尝试连最简单的事情时，例如遍历矩阵行等，我总是遇到涉及'Nat'的证明问题。 –

答

从评论中，我担心我一定会错过一些非常明显的东西，但这是我的承诺。整点：

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 a 0当函数一般返回类型Vec a n，需要专门的n到0，并GADTs模式匹配提供了一种方法来做到这一点，只要你有一个构造函数，如SZero，这意味着n ~ 0。

现在单身包中的SNat没有这样的构造函数。就我所知，获得一个唯一的方法是为自然构建一个全新的单体类型并实现必要的类型族。也许你可以用包装Nat的方式做到这一点，所以你比一个Peano建筑更接近SZero :: Sing (SN 0)，SNonZero :: Sing (SN n)，但我不知道。

当然，还有另一种方法来专门化返回Vec a n返回Vec a 0的函数，即类型类。

如果您愿意放弃一些显式的单例机制并切换到类型类（并且还允许重叠和不可判定的实例），以下内容似乎可行。我不得不稍微修改V的定义以使用n :- 1而不是n :+ 1，但我并不认为认为存在问题。

{-# 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上使用模式匹配的地方（如果它是归纳定义的）。不得不使用额外的类型类型有点难看，但它解决了我所遇到的实际问题。我估计在盯着它太久之后，我开发出了一些隧道视野。无论如何，除非在接下来的日子里出现更好的解决方案，否则我会很高兴地给你奖励。 –

答

在这里玩有两种天然的概念。一个是“文字自然”（即0,1,2等），另一个是“Peano naturals”（即Z，S Z，S（S Z）等）。这篇论文正在使用的显然是Peano天然植物，但一个单身人士使用的是字面自然。

幸运的是，还有另一个名为type-natural的软件包，它定义了Peano天然植物以及conversion to literal naturals和conversion from literal naturals。

如何解构SNAT（单身）

相关推荐