使用haskell的单例，我怎么写'fromList :: [a] - > Vec a n``？

本文介绍了使用haskell的单例，我怎么写'fromList :: [a] - &gt; Vec a n``？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述 作为理解 singletons 的一部分，我试图弥合编译时间安全性和将运行时值提升到相关类型安全性之间的差距。 我认为尽管运行时值的最小示例是一个函数，它接受一个无界列表，并将其转换为大小索引的向量。下面的框架提供了长度索引的向量，但我不能完全确定如何从写入。 I { - ＃LANGUAGE GADTs＃ - } { - ＃LANGUAGE ScopedTypeVariables＃ - } { - ＃LANGUAGE TemplateHaskell＃ - } { - ＃LANGUAGE TypeFamilies＃ - } { - ＃LANGUAGE TypeInType＃ - } { - ＃LANGUAGE UndecidableInstances＃ - } import Data.Singletons import Data.Singletons.TH $（singletons [ d | data Nat = Z | S Nat推导（显示） |]） 数据Vec an其中无:: Vec a Z 缺点：a - > Vec a n - > Vec a（S n） 实例Show a => Show（Vec an）其中显示Nil =Nil show（Cons x xs）= show x ++：<++ show xs fromListExplicit： ：forall（n :: Nat）a。 SNat n - > [a] - > Vec a fromListExplicit SZ _ =无 fromListExplicit（SS n）（x：xs）= Cons x（fromListExplicit n xs） ex1 = fromListExplicit（SS（SS SZ）））[1..99] - 1：< 2： 3：无 fromListImplicit ::（?????）=> [a] - > Vec a n fromListImplicit = ????? main :: IO（） main = do xs< - readLn :: IO [Int] print $ fromListImplicit xs 解决方案这是 not 可能使用Haskell，因为Haskell不会还有完全依赖类型（尽管GHC 将来可能会使用）。请注意， fromList :: [a] - > Vec a 既有 a 和 n 通用量化，这意味着用户应该能够选择他们的 n 并取回 Vec 大小合适。这是没有意义的！诀窍是 n 并不真正让用户选择 - 它必须是输入列表的长度。 （出于同样的原因，来自List :: Integer - > [a] - > Vec和的不会更有用 - 大小提示必须是类型化的， ） 寻找像Idris这样的依赖类型语言，您可以定义 fromList：（l：List elem） - > Vec（长度为l）elem 实际上它们是在标准库中定义这个。 那么，你可以做什么？不言而喻， Vec 的长度等于输入列表的大小（需要将输入列表的长度提升到类型级别），您可以说具有一些长度。 data SomeVec a where {SomeVec :: Vec an - > SomeVec a} list2SomeVec :: [a] - > SomeVec a list2SomeVec [] = SomeVec Nil list2SomeVec（x：xs）= case list2SomeVec xs of SomeVec ys - > SomeVec（x`Cons` ys） 这并不是非常有用，但它总比没有好。 As part of my journey in understanding singletons I have tried to bridge the gap between compile time safety, and lifting runtime values into that dependent type safety.I think though that a minimal example of "runtime" values is a function that takes an unbounded list, and converts it to a size-indexed vector. The following skeleton provides length-indexed vectors, but I can't quite determine how to write fromList.I have considered making the function take a size parameter, but I suspect it's possible to keep that implicit.{-# LANGUAGE GADTs #-}{-# LANGUAGE ScopedTypeVariables #-}{-# LANGUAGE TemplateHaskell #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE TypeInType #-}{-# LANGUAGE UndecidableInstances #-}import Data.Singletonsimport Data.Singletons.TH$(singletons [d| data Nat = Z | S Nat deriving (Show) |])data Vec a n where Nil :: Vec a Z Cons :: a -> Vec a n -> Vec a (S n)instance Show a => Show (Vec a n) where show Nil = "Nil" show (Cons x xs) = show x ++ " :< " ++ show xsfromListExplicit :: forall (n :: Nat) a. SNat n -> [a] -> Vec a nfromListExplicit SZ _ = NilfromListExplicit (SS n) (x : xs) = Cons x (fromListExplicit n xs)ex1 = fromListExplicit (SS (SS (SS SZ))) [1..99]-- 1 :< 2 :< 3 :< NilfromListImplicit :: (?????) => [a] -> Vec a nfromListImplicit = ?????main :: IO ()main = do xs <- readLn :: IO [Int] print $ fromListImplicit xs 解决方案 This is not possible using Haskell because Haskell does not yet have full dependent types (although GHC might in the future). Notice thatfromList :: [a] -> Vec a nHas both a and n quantified universally, which means that the user should be able to pick their n and get back a Vec of the right size. That makes no sense! The trick is that n is not really for the user to choose - it has to be the length of the input list. (For the same reason, fromList :: Integer -> [a] -> Vec a n would not be any more useful - the size hint has to be something type-level.)Looking to a dependently typed language like Idris, you can definefromList : (l : List elem) -> Vec (length l) elemAnd in fact they define this in the standard library.So, what can you do? Short of saying that Vec has the length equal to the size of the input list (which requires lifting "length of the input list" to the type level), you can say it has some length.data SomeVec a where { SomeVec :: Vec a n -> SomeVec a }list2SomeVec :: [a] -> SomeVec alist2SomeVec [] = SomeVec Nillist2SomeVec (x:xs) = case list2SomeVec xs of SomeVec ys -> SomeVec (x `Cons` ys)That isn't spectacularly useful, but it is better than nothing. 这篇关于使用haskell的单例，我怎么写'fromList :: [a] - &gt; Vec a n``？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！