AQueue.hs

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, OverlappingInstances, ScopedTypeVariables, TemplateHaskell, FlexibleContexts, UndecidableInstances #-}
import Prelude hiding (head)
import GHC.TypeLits
import Acme.NumberSystem

numberSystem 10

newtype Queue (k :: Nat) v = Queue [v] deriving (Show)

empty :: Queue 0 a
empty = Queue []

add :: v -> Queue ks v -> Queue (Add ks 1) v
add v (Queue xs) = Queue (v:xs)

class Ke (k :: Nat) v where
  head :: Queue k v -> (v, Queue (Sub k 1) v)

instance (1 <= k) => Ke k v where
  head (Queue (x:xs)) = (x, Queue xs)

-- test

foo = add 10 $ add 2 $ add 1 empty

ok =        snd . head . snd . head . snd . head $ foo
-- ohno = head snd . head . snd . head . snd . head $ foo -- type error