要素数を保持するVector型

Idrisの場合

import Data.Vect

code:idr

data 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の方ねmrsekut.icon

index :: forall n a. Vector n a -> Finite n -> a

generate :: forall n a. KnownNat n => (Finite n -> a) -> Vector n a

code:hs

v = 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の普通の使い方がわからんmrsekut.icon