Здравствуйте, WolfHound, Вы писали:

WH>Код на хаскеле который читает с консоли число и создаёт вектор тип которого зависит этого числа в студию.

Извините, что встреваю в вашу цивилизованную ученую дискуссию, но такой код как раз несложно пишется:

{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies #-}
module Main where

-- натуральные числа по Пеано
data Nat = Z | S Nat deriving (Show, Eq, Ord)

-- вектор, индексированный натуральной длиной
data Vec :: Nat -> * -> * where
   V0    ::                  Vec Z x
   (:>)  :: x -> Vec n x ->  Vec (S n) x

infixr 5 :>

-- это к задаче не относится, но чисто ради фана сделаем сложение чисел и конкатенацию векторов
type family (m :: Nat) :+ (n :: Nat) :: Nat
type instance  Z    :+  n  =  n
type instance  S m  :+  n  =  S (m :+ n)

vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
vappend  V0         ys  =  ys
vappend  (x :> xs)  ys  =  x :> vappend xs ys

toList :: Vec n a -> [a]
toList V0 = []
toList (x :> xs) = x : toList xs

-- семейство синглтон типов: по одному рантайм-значению для каждого типового натурального числа
data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

-- сделать вектор заданной длины
makeVec :: Natty n -> a -> Vec n a
makeVec Zy _ = V0
makeVec (Sy k) x = x :> makeVec k x

-- тут самая мякотка: получаем рантайм значение, делаем вектор такой длины и показываем
test :: Int -> IO ()
test n = loop n Zy where   -- цикл нужен, чтобы получить натуральное число из инта
  loop :: Int -> Natty m -> IO ()
  loop 0 m = print $ toList $ makeVec m 7
  loop k m = loop (k-1) (Sy m)

--запрашиваем число из консоли, показываем вектор из указанного пользователем количества семерок
main :: IO ()
main = do
  putStrLn "enter n:"
  nstr <- getLine   
  test $ read nstr

enter n:
5
[7,7,7,7,7]