PolyKindsOnly.hs

{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, DataKinds, PolyKinds #-}
-- We can also just add TypeInType, and skip DataKinds and KindSignatures,
-- since TypeInType enables both of those, PolyKinds (and more!)
module Main where

import Data.Kind (Type)

-- Define a Type for the natural numbers, Zero and a successor
data Nat = Z | S Nat

class Addable k where
  type (a :: k) + (b :: k) :: k

instance Addable Nat where
  type (Z + a) = a
  type (S a + b) = S (a + b)

infixr 5 :.

data Vect :: Nat -> Type -> Type where
  Nil :: Vect Z a
  (:.) :: a -> Vect n a -> Vect (S n) a

app :: Vect n a -> Vect m a -> Vect (n + m) a
app Nil a = a
app (a :. as) bs = a :. (app as bs)

vhead :: Vect (S k) a -> a
vhead (a :. v) = a

ex1 :: Vect (S (S Z)) Int
ex1 = 1 :. 2 :. Nil

ex2 :: Vect (S Z) Int
ex2 = 1 :. Nil

ex3 :: Vect (S (S (S Z))) Int
ex3 = ex1 `app` ex2

empty :: Vect Z ()
empty = Nil

main :: IO ()
main = print $ vhead ex3