/mrsekut-p/要素数を保持するVector型

generated at 2/18/2025, 4:58:35 PM
要素数を保持するVector型

Idrisの場合
 import Data.Vect 
idrdata Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   (::) : a -> Vect k a -> Vect (S k) a
NatやVectの使い方などはIdrisの型を参照




hsの場合
通常のHaskellのVector型ではなく、vector-sizedの方ね
https://hackage.haskell.org/package/vector-sized
Data.Vector.Sized
 index :: forall n a. Vector n a -> Finite n -> a 
 generate :: forall n a. KnownNat n => (Finite n -> a) -> Vector n a 
hsv = V.fromTuple ("hey", "what's", "going", "on") -- :: V.Vector 4 String
a = V.index v 1 -- "what's"
b = V.generate (\i -> V.index v (i-2)) -- ["going","on","hey","what's"]
c = V.generate (V.index v)             -- ["hey","what's","going","on"]
generateの普通の使い方がわからん