blob: ab79bd679949401c55d5a26c681d40c826c60ef5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
module PolyKinds01 where
import Data.Kind (Type)
data Nat = Ze | Su Nat
data Vec :: Type -> Nat -> Type where
VNil :: Vec a Ze
VCons :: a -> Vec a n -> Vec a (Su n)
vec :: Vec Nat (Su Ze)
vec = VCons Ze VNil
|
