FIn.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Fin where

data Nat = Z | S Nat

newtype Fin (n :: Nat) = Fin { unFin :: Int }

pattern FZ :: Fin ('S n)
pattern FZ = Fin 0

pattern FS :: Fin n -> Fin ('S n)
pattern FS f <- (finPred -> Just f)
  where FS = finSucc

finPred :: Fin ('S n) -> Maybe (Fin n)
finPred (Fin 0) = Nothing
finPred (Fin i) = Just (Fin (pred i))

finSucc :: Fin n -> Fin ('S n)
finSucc (Fin i) = Fin (succ i)

x :: Int
x = case FZ of { FS (Fin i) -> i ; _ -> 1 }