Vec.hs

{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeInType, TypeOperators,
             TypeFamilies, GADTs, UndecidableInstances, InstanceSigs #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}

import Data.Kind
import Data.Singletons.TH
import Data.Singletons.Prelude
import Prelude hiding ( take )

$(singletons [d|
  data Nat = Zero | Succ Nat
    deriving (Eq)

   -- the derived instance doesn't have the right recursive structure
  instance Ord Nat where
    Zero   `compare` Zero = EQ
    Succ _ `compare` Zero = GT
    Zero   `compare` Succ _ = LT
    Succ n `compare` Succ m = n `compare` m

    Zero   <= Zero   = True
    Zero   <= Succ _ = True
    Succ _ <= Zero   = False
    Succ n <= Succ m = n <= m

  instance Num Nat where
    Zero   + m = m
    Succ n + m = Succ (n + m)

    Zero   - _      = Zero   -- truncate subtraction
    n      - Zero   = n
    Succ n - Succ m = n - m

    Zero   * _ = Zero
    Succ n * m = m + (n * m)

    negate = const Zero     -- truncate negatives

    abs = id
    signum = id

    fromInteger n | n == 0    = Zero
                  | n > 0     = Succ (fromInteger (n-1))
                  | otherwise = error "No negative Nats"
  |])

data Vec :: Type -> Nat -> Type where
  Nil  :: Vec a Zero
  (:>) :: a -> Vec a n -> Vec a (Succ n)
infixr 5 :>

type Π = Sing   -- because I can

take :: ((i :<= n) ~ True) => Π (i :: Nat) -> Vec a n -> Vec a i
take SZero     _         = Nil
take (SSucc i) (x :> xs) = x :> take i xs

slice :: ((i :<= j) ~ True, (j :<= n) ~ True) => Π (i :: Nat) -> Π (j :: Nat) -> Vec a n -> Vec a (j :- i)
slice SZero     j         vec       = take j vec
slice (SSucc i) (SSucc j) (_ :> xs) = slice i j xs