Haskell function with length-indexed vector and predicate constraint

Question

Here is function f that takes only length indexed vector with length exacly 2.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module Main where 
data Nat = Z | S Nat deriving Show
type One = S Z
type Two = S One

data Vec :: Nat -> * -> * where
  Nil  :: Vec Z a
  (:>) :: a -> Vec n a -> Vec (S n) a 

f :: (l ~ Two) => Vec l a -> a
f (e :> _) = e

What is the best way to write function which only takes list of length greater (or less) then 2 ? So something like:

f :: (Gt l Two) => Vec l a -> a
f (e :> _) = e

Answer 1

You can define your own Gt using type families.

type Gt :: Nat -> Nat -> Constraint
type family Gt n m where
  Gt Z _ = 'True ~ 'False
  Gt _ Z = ()
  Gt (S n) (S m) = Gt n m

Then, you can write f using a constraint.

f :: (Gt l Two) => Vec l a -> a
f (e :> _) = e

But I'm not sure if this is better than this.

f' :: Vec (S (S (S n))) a -> a
f' (e :> _) = e

Of course, it'd be cleaner to write (Gt l Hundred) => ... than Vec (S (S (S ....))) a ..., but you still need to write Hundred anyway.