Minimal.idr

data IsEven : (b : Bool) -> Type where
  ItIsEven : IsEven True
  
Uninhabited (IsEven False) where
  uninhabited IsEven impossible

itHasTheOneBitSet : (n : Nat) -> Bool
itHasTheOneBitSet Z = False
itHasTheOneBitSet (S Z) = True
itHasTheOneBitSet (S (S a)) = itHasTheOneBitSet a

itIsEven : (n : Nat) -> Type
itIsEven n =
  IsEven (not (itHasTheOneBitSet n))

infixr 10 ::@

data Vect : Nat -> Type -> Type where
  VNil  : Vect Z a
  (::@) : a -> Vect k a -> Vect (S k) a

record EvenVect (n : Nat) t where
  constructor MkEvenVect
  iseven : itIsEven n
  items : Vect n t

div2 : Nat -> Nat
div2 Z = Z
div2 (S Z) = Z
div2 (S (S k)) = S (div2 k)

{- Type-unsafe map -}
map2unsafe : (t -> t -> u) -> Vect n t -> Vect (div2 n) u
map2unsafe f ((::@) a ((::@) b tail)) = (f a b) ::@ (map2unsafe f tail)
map2unsafe _ ((::@) _ VNil) = VNil
map2unsafe _ VNil = VNil

map2 : (t -> t -> u) -> EvenVect n t -> Vect (div2 n) u
map2 f v =
  map2unsafe f (items v)

mapped : Vect (S Z) String
mapped = 
  map2 
    (\a,b => a ++ b) 
    (MkEvenVect ItIsEven ("hi" ::@ "there" ::@ VNil))

{-
mappedNo : Vect (S Z) String
mappedNo = 
  map2 
    (\a,b => a ++ b) 
    (MkEvenVect ItIsEven ("hi" ::@ "there" ::@ "you" ::@ VNil))
-}

mappedYes : Vect (S (S Z)) String
mappedYes = 
  map2 
    (\a,b => a ++ b) 
    (MkEvenVect ItIsEven ("hi" ::@ "there" ::@ "you" ::@ "nerd" ::@ VNil))