相关疑难解决方法(0)

我正在尝试使用GHC.TypeLits,singletons和constraints中的机制为长度索引列表编写复制函数.

该Vect类型和签名replicateVec给出如下:

data Vect :: Nat -> Type -> Type where
  VNil  :: Vect 0 a
  VCons :: a -> Vect (n - 1) a -> Vect n a

replicateVec :: forall n a. SNat n -> a -> Vect n a

你怎么写这个replicateVec功能？

我有一个replicateVec编译和类型检查的版本,但它似乎在运行时进入无限循环.代码如下.我添加了评论,试图使我使用的法律和证据更容易理解:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE …