blob: f698d5d687b313df2733e1fabe898d24843259a4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
{-# LANGUAGE DataKinds, PolyKinds, UnicodeSyntax, GADTs, NoImplicitPrelude,
TypeOperators, TypeFamilies, StandaloneKindSignatures #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module TypeLevelVec where
import Data.Kind
data ℕ ∷ Type where
O ∷ ℕ
S ∷ ℕ → ℕ
type family x + y where
O + n = n
S m + n = S (m + n)
infixl 5 +
data Vec ∷ ℕ → Type → Type where
Nil ∷ Vec O a
(:>) ∷ a → Vec n a → Vec (S n) a
infixr 8 :>
type (++) :: Vec n a -> Vec m a -> Vec (n + m) a
type family x ++ y where
Nil ++ y = y
(x :> xs) ++ y = x :> (xs ++ y)
infixl 5 ++
|
