Skip to content

Instantly share code, notes, and snippets.

@goldfirere
Last active December 5, 2016 13:50
Show Gist options
  • Save goldfirere/013a71f3775a09c7ff2f3980f4d54133 to your computer and use it in GitHub Desktop.
Save goldfirere/013a71f3775a09c7ff2f3980f4d54133 to your computer and use it in GitHub Desktop.
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment