FinNat.hs

{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

module Fin where

import GHC.TypeLits

data Vec :: Nat -> * -> * where
    Nil  :: Vec 0 a
    (:#) :: a -> Vec n a -> Vec (1 + n) a

infixr 5 :#

data Fin :: Nat -> * where
  FZ :: Fin k
  FS :: Fin k -> Fin (1 + k)

index :: Vec (1 + n) a -> Fin n -> a
index (x:#_) FZ = x
index (_:#xs) (FS s) = index xs s