Haskell 单例：typelits 包

Question

我很难让编译器相信我的类型是正确的。Nat对于带有Zero和构造函数的常规\n 来说，Succ这非常简单（目标是replicate为长度索引列表编写函数（Vect ) 编写函数）：

\n\n

replicate' :: SNat n -> a -> Vect n a\nreplicate' SZero _ = Nil\nreplicate' (SSucc n) a = a :> replicate' n a\n

\n\n

但经常Nat非常慢。

\n\n

因此，在单例库中有一个镜像 GHC.TypeLits 的包，以实现更快的 Nats。\n但我无法使上面的示例与它一起使用：

\n\n

sameNat :: forall a b. (KnownNat a, KnownNat b) => SNat a -> SNat b -> Maybe (a :~: b)\nsameNat x y\n  | natVal (Proxy :: Proxy a) == natVal (Proxy :: Proxy b) = Just (unsafeCoerce Refl)\n  | otherwise            = Nothing\n\nreplicate'' :: (KnownNat n) => SNat n -> a -> Vect n a\nreplicate'' n a =\n  case sameNat n (sing :: Sing 0) of\n    Just Refl -> Nil\n    Nothing   -> a ::> replicate'' (sPred n) a\n

\n\n

这不会在最后一行进行类型检查：

\n\n

Couldn't match type \xe2\x80\x98n\xe2\x80\x99\n                     with \xe2\x80\x98(n GHC.TypeNats.- 1) GHC.TypeNats.+ 1\xe2\x80\x99\n

\n

Answer 1

据我所知，您所采取的确切方法无法按您想要的方式工作。 sameNat在运行时评估，因此类型检查器无法使用其“决策”，因此类型检查器无法基于区分 case 构造的两个分支来执行任何类型推断。

您可能对我对How to deconstruct an SNat (singletons)的回答感兴趣 ，关于类似的问题，它提供了一种unsafeCoerce完全避免使用类型类的实现。然而，正如 @Ben 在评论中指出的那样，由于使用了类型类，n每当定义大小向量时，编译器都必须遵循一系列实例定义（并且编译后的代码可能显式包含嵌套实例n的结构）n字典）使得这对于真实代码来说不切实际。例如，一百万个元素向量可能会导致编译器运行太长时间和/或使用太多内存而无法接受。

对于真实的代码，我建议手动进行类型检查（即验证编写的代码是否类型安全）并强制执行unsafeCoerce：

replicate1 :: (KnownNat n) => SNat n -> a -> Vect n a
replicate1 n a =
  unsafeCoerce (iterate (unsafeCoerce . (a ::>)) Nil
                !! fromInteger (fromSing n))

显然，这个定义错过了这个特定定义的依赖类型的要点，但希望您可以构建一组可信（手动类型检查）原语，然后在它们之上构建可以受益于的重要算法更严格的型式检查。

请注意，在这种特殊情况下，您甚至不需要该n参数，因此您可以编写：

{-# LANGUAGE ScopedTypeVariables #-}

replicate2 :: forall a n . (KnownNat n) => a -> Vect n a
replicate2 a =
  unsafeCoerce (iterate (unsafeCoerce . (a ::>)) Nil
        !! fromInteger (fromSing (SNat :: SNat n)))

无论如何，一个完整的工作示例是：

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
import Unsafe.Coerce

infixr 5 ::>
data Vect (n :: Nat) a where
  Nil :: Vect 0 a
  (::>) :: a -> Vect (n :- 1) a -> Vect n a

instance (Show a) => Show (Vect n a) where
  showsPrec _ Nil = showString "Nil"
  showsPrec d (x ::> xs) = showParen (d > prec) $
showsPrec (prec+1) x . showString " ::> " . showsPrec prec xs
where prec=5

replicate1 :: (KnownNat n) => SNat n -> a -> Vect n a
replicate1 n a =
  unsafeCoerce (iterate (unsafeCoerce . (a ::>)) Nil
        !! fromInteger (fromSing n))

replicate2 :: forall a n . (KnownNat n) => a -> Vect n a
replicate2 a =
  unsafeCoerce (iterate (unsafeCoerce . (a ::>)) Nil
        !! fromInteger (fromSing (SNat :: SNat n)))

head' :: Vect (n :+ 1) a -> a
head' (x ::> _) = x

tail' :: ((n :+ 1) :- 1) ~ n => Vect (n :+ 1) a -> Vect n a
tail' (_ ::> v) = v

main = do print (replicate2 False   :: Vect 0 Bool)
          print (replicate2 "Three" :: Vect 3 String)
          print (head' (tail' (replicate2 "1M" :: Vect 1000000 String)))

          print (replicate1 (SNat :: SNat 0) False   :: Vect 0 Bool)
          print (replicate1 (SNat :: SNat 3) "Three" :: Vect 3 String)
          print (head' (tail' (replicate1 (SNat :: SNat 1000000) "1M" :: Vect 1000000 String)))