Моему другу Серёже Алирзаеву посвящается…

> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE StandaloneDeriving #-}
> {-# LANGUAGE DeriveFunctor #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE DeriveTraversable #-}

> import Data.Foldable
> import Data.Proxy

> import GHC.TypeLits

> data Peano = Z | S Peano
>     deriving Show

> data FixedList (n :: Peano) a where
>     Nil  :: FixedList Z a
>     (:.) :: a -> FixedList n a -> FixedList (S n) a

> infixr 5 :.

> deriving instance Show a => Show (FixedList n a)
> deriving instance Eq a => Eq (FixedList n a)
> deriving instance Functor (FixedList n)
> deriving instance Foldable (FixedList n)
> deriving instance Traversable (FixedList n)

λ> fmap (+1) (1 :. 2 :. 3 :. Nill)
-- (2 :. 3 :. 4 :. Nill)

λ> find (==2) (1 :. 2 :. 3 :. Nill)
-- Just 2

λ> mapM_ print (1 :. 2 :. 3 :. Nill)
-- 1
-- 2
-- 3

sumOurSpecialFixedList :: Num a =>
     FixedList
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
       a
     -> a
sumOurSpecialFixedList = sum

> type family N2P (n :: Nat) where
>     N2P 0 = Z
>     N2P n = S (N2P (n - 1))

> type FList n = FixedList (N2P n)

sumOurSpecialFixedList :: Num a => FList 20 a -> a
sumOurSpecialFixedList = sum

λ> (1 :. 2 :. 3 :. Nil) !! 1

<interactive>:2:2:
    Couldn't match expected type ‘[a]’
                with actual type ‘FixedList ('S ('S ('S 'Z))) Integer’
    Relevant bindings include it :: a (bound at <interactive>:2:1)
    In the first argument of ‘(!!)’, namely ‘(1 :. 2 :. 3 :. Nil)’
    In the expression: (1 :. 2 :. 3 :. Nil) !! 1
    In an equation for ‘it’: it = (1 :. 2 :. 3 :. Nil) !! 1

> type family P2N (n :: Peano) where
>     P2N Z     = 0
>     P2N (S n) = 1 + P2N n

> findex :: (KnownNat n, n + 1 <= P2N m) => Proxy n -> FixedList m a -> a
> findex proxy xs = toList xs !! fromInteger (natVal proxy)

λ> :set -XDataKinds
λ> findex  (Proxy :: Proxy 2) (1 :. 2 :. 3 :. Nil)
-- 3
λ> findex  (Proxy :: Proxy 0) (1 :. 2 :. 3 :. Nil)
-- 1