PolyKinds01.hs 319 Bytes
Newer Older
dreixel's avatar
dreixel committed
1 2
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE KindSignatures             #-}
dreixel's avatar
dreixel committed
3 4 5 6 7 8 9 10 11 12 13 14
{-# LANGUAGE GADTs                      #-}

module PolyKinds01 where

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  VNil  :: Vec a Ze
  VCons :: a -> Vec a n -> Vec a (Su n)

vec :: Vec Nat (Su Ze)
vec = VCons Ze VNil