{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts#-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-} -- for ReverseLoop type family
module Data.HVect
  ( -- * typesafe strict vector
    HVect (..)
  , empty, null, head, tail
  , singleton
  , length, HVectLen
  , findFirst, InList, ListContains, NotInList
  , MaybeToList
  , (!!), HVectIdx
  , HVectElim
  , Append, (<++>)
  , ReverseLoop, Reverse, reverse
  , uncurry
  , Rep (..), HasRep (..)
  , curryExpl, curry
  , packExpl, pack
    -- * type class constraints on list elements
  , AllHave
    -- * type level numeric utilities
  , Nat (..), SNat (..), sNatToInt
  , intToSNat, AnySNat (..)
  , (:<)
  ) where

import GHC.Exts
import Prelude hiding (reverse, uncurry, curry, head, null, (!!), length, tail)

-- | Heterogeneous vector
data HVect (ts :: [*]) where
  HNil :: HVect '[]
  (:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)

infixr 5 :&:

instance Eq (HVect '[]) where
    HVect '[]
_ == :: HVect '[] -> HVect '[] -> Bool
== HVect '[]
_ =
        Bool
True

instance (Eq (HVect ts), Eq t) => Eq (HVect (t ': ts)) where
    t
a :&: HVect ts
as == :: HVect (t : ts) -> HVect (t : ts) -> Bool
== t
b :&: HVect ts
bs =
        t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
t
b Bool -> Bool -> Bool
&& HVect ts
as HVect ts -> HVect ts -> Bool
forall a. Eq a => a -> a -> Bool
== HVect ts
HVect ts
bs

instance Show (HVect '[]) where
    showsPrec :: Int -> HVect '[] -> ShowS
showsPrec Int
d HVect '[]
HNil =
        Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"[]"

instance (Show (HVect ts), Show t) => Show (HVect (t ': ts)) where
    showsPrec :: Int -> HVect (t : ts) -> ShowS
showsPrec Int
d (t
a :&: HVect ts
as) =
        Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
           Int -> t -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 t
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
           String -> ShowS
showString String
" <:> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
           Int -> HVect ts -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 HVect ts
as

instance Ord (HVect '[]) where
    HVect '[]
_ compare :: HVect '[] -> HVect '[] -> Ordering
`compare` HVect '[]
_ = Ordering
EQ
    HVect '[]
_ <= :: HVect '[] -> HVect '[] -> Bool
<= HVect '[]
_ = Bool
True

instance (Ord (HVect ts), Ord t) => Ord (HVect (t ': ts)) where
    (t
a :&: HVect ts
as) compare :: HVect (t : ts) -> HVect (t : ts) -> Ordering
`compare` (t
b :&: HVect ts
bs) =
        case t
a t -> t -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` t
t
b of
          Ordering
EQ -> HVect ts
as HVect ts -> HVect ts -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` HVect ts
HVect ts
bs
          Ordering
o -> Ordering
o
    t
a :&: HVect ts
as <= :: HVect (t : ts) -> HVect (t : ts) -> Bool
<= t
b :&: HVect ts
bs =
        t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
t
b Bool -> Bool -> Bool
&& HVect ts
as HVect ts -> HVect ts -> Bool
forall a. Ord a => a -> a -> Bool
<= HVect ts
HVect ts
bs

type family HVectElim (ts :: [*]) (a :: *) :: * where
    HVectElim '[] a = a
    HVectElim (t ': ts) a = t -> HVectElim ts a

type family Append (as :: [*]) (bs :: [*]) :: [*] where
    Append '[] bs = bs
    Append (a ': as) bs = a ': (Append as bs)

type family InList (x :: *) (xs :: [*]) :: Nat where
    InList x (x ': ys) = 'Zero
    InList x (y ': ys) = 'Succ (InList x ys)

type family AllHave (c :: * -> Constraint) (xs :: [*]) :: Constraint where
    AllHave c '[] = 'True ~ 'True
    AllHave c (x ': xs) = (c x, AllHave c xs)

class SNatRep n where
    getSNat :: SNat n

instance SNatRep 'Zero where
    getSNat :: SNat 'Zero
getSNat = SNat 'Zero
SZero

instance SNatRep n => SNatRep ('Succ n) where
    getSNat :: SNat ('Succ n)
getSNat = SNat n -> SNat ('Succ n)
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat n
forall (n :: Nat). SNatRep n => SNat n
getSNat

type family NotInList (x :: *) (xs :: [*]) :: Bool where
    NotInList x (x ': ys) = 'False
    NotInList x (y ': ys) = NotInList x ys
    NotInList x '[] = 'True

type ListContains n x ts = (SNatRep n, InList x ts ~ n, HVectIdx n ts ~ x)

type family MaybeToList (a :: Maybe *) :: [*] where
    MaybeToList ('Just r) = '[r]
    MaybeToList 'Nothing = '[]

-- | Find first element in 'HVect' of type x
findFirst :: forall x ts n. (ListContains n x ts) => HVect ts -> x
findFirst :: HVect ts -> x
findFirst HVect ts
vect = SNat n
idx SNat n -> HVect ts -> HVectIdx n ts
forall (n :: Nat) (as :: [*]). SNat n -> HVect as -> HVectIdx n as
!! HVect ts
vect
    where
      idx :: SNat n
      idx :: SNat n
idx = SNat n
forall (n :: Nat). SNatRep n => SNat n
getSNat

singleton :: a -> HVect '[a]
singleton :: a -> HVect '[a]
singleton a
el = a
el a -> HVect '[] -> HVect '[a]
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
:&: HVect '[]
HNil

empty :: HVect '[]
empty :: HVect '[]
empty = HVect '[]
HNil

null :: HVect as -> Bool
null :: HVect as -> Bool
null HVect as
HNil = Bool
True
null HVect as
_ = Bool
False

head :: HVect (t ': ts) -> t
head :: HVect (t : ts) -> t
head (t
a :&: HVect ts
_) = t
t
a

tail :: HVect (t ': ts) -> HVect ts
tail :: HVect (t : ts) -> HVect ts
tail (t
_ :&: HVect ts
as) = HVect ts
HVect ts
as

length :: HVect as -> SNat (HVectLen as)
length :: HVect as -> SNat (HVectLen as)
length HVect as
HNil = SNat (HVectLen as)
SNat 'Zero
SZero
length (t
_ :&: HVect ts
as) = SNat (HVectLen ts) -> SNat ('Succ (HVectLen ts))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc (HVect ts -> SNat (HVectLen ts)
forall (as :: [*]). HVect as -> SNat (HVectLen as)
length HVect ts
as)

sNatToInt :: SNat n -> Int
sNatToInt :: SNat n -> Int
sNatToInt SNat n
SZero = Int
0
sNatToInt (SSucc SNat n
n) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (SNat n -> Int
forall (n :: Nat). SNat n -> Int
sNatToInt SNat n
n)

intToSNat :: Int -> AnySNat
intToSNat :: Int -> AnySNat
intToSNat Int
0 = SNat 'Zero -> AnySNat
forall (n :: Nat). SNat n -> AnySNat
AnySNat SNat 'Zero
SZero
intToSNat Int
n =
    case Int -> AnySNat
intToSNat (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) of
      AnySNat SNat n
m -> SNat ('Succ n) -> AnySNat
forall (n :: Nat). SNat n -> AnySNat
AnySNat (SNat n -> SNat ('Succ n)
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat n
m)

data Nat where
    Zero :: Nat
    Succ :: Nat -> Nat

data SNat (n :: Nat) where
    SZero :: SNat 'Zero
    SSucc :: SNat n -> SNat ('Succ n)

data AnySNat where
    AnySNat :: forall n. SNat n -> AnySNat

type family HVectLen (ts :: [*]) :: Nat where
    HVectLen '[] = 'Zero
    HVectLen (t ': ts) = 'Succ (HVectLen ts)

type family HVectIdx (n :: Nat) (ts :: [*]) :: * where
    HVectIdx 'Zero (a ': as) = a
    HVectIdx ('Succ n) (a ': as) = HVectIdx n as

type family (m :: Nat) :< (n :: Nat) :: Bool where
    m :< 'Zero = 'False
    'Zero :< ('Succ n) = 'True
    ('Succ m) :< ('Succ n) = m :< n

type family (m :: Nat) :- (n :: Nat) :: Nat where
    n :- 'Zero = n
    ('Succ m) :- ('Succ n) = m :- n

(!!) :: SNat n -> HVect as -> HVectIdx n as
SNat n
SZero !! :: SNat n -> HVect as -> HVectIdx n as
!! (t
a :&: HVect ts
_) = t
HVectIdx n as
a
(SSucc SNat n
s) !! (t
_ :&: HVect ts
as) = SNat n
s SNat n -> HVect ts -> HVectIdx n ts
forall (n :: Nat) (as :: [*]). SNat n -> HVect as -> HVectIdx n as
!! HVect ts
as
SNat n
_ !! HVect as
_ = String -> HVectIdx n as
forall a. HasCallStack => String -> a
error String
"HVect !!: This should never happen"

infixr 5 <++>
infixl 9 !!

(<++>) :: HVect as -> HVect bs -> HVect (Append as bs)
<++> :: HVect as -> HVect bs -> HVect (Append as bs)
(<++>) HVect as
HNil HVect bs
bs = HVect bs
HVect (Append as bs)
bs
(<++>) (t
a :&: HVect ts
as) HVect bs
bs = t
a t -> HVect (Append ts bs) -> HVect (t : Append ts bs)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
:&: (HVect ts
as HVect ts -> HVect bs -> HVect (Append ts bs)
forall (as :: [*]) (bs :: [*]).
HVect as -> HVect bs -> HVect (Append as bs)
<++> HVect bs
bs)

type family ReverseLoop (as :: [*]) (bs :: [*]) :: [*] where
    ReverseLoop '[] bs = bs
    ReverseLoop (a ': as) bs = ReverseLoop as (a ': bs)

type Reverse as = ReverseLoop as '[]

reverse :: HVect as -> HVect (Reverse as)
reverse :: HVect as -> HVect (Reverse as)
reverse HVect as
vs = HVect as -> HVect '[] -> HVect (Reverse as)
forall (as :: [*]) (bs :: [*]).
HVect as -> HVect bs -> HVect (ReverseLoop as bs)
go HVect as
vs HVect '[]
HNil
  where
    go :: HVect as -> HVect bs -> HVect (ReverseLoop as bs)
    go :: HVect as -> HVect bs -> HVect (ReverseLoop as bs)
go HVect as
HNil HVect bs
bs = HVect bs
HVect (ReverseLoop as bs)
bs
    go (t
a :&: HVect ts
as) HVect bs
bs = HVect ts -> HVect (t : bs) -> HVect (ReverseLoop ts (t : bs))
forall (as :: [*]) (bs :: [*]).
HVect as -> HVect bs -> HVect (ReverseLoop as bs)
go HVect ts
as (t
a t -> HVect bs -> HVect (t : bs)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
:&: HVect bs
bs)

uncurry :: HVectElim ts a -> HVect ts -> a
uncurry :: HVectElim ts a -> HVect ts -> a
uncurry HVectElim ts a
f HVect ts
HNil = a
HVectElim ts a
f
uncurry HVectElim ts a
f (t
x :&: HVect ts
xs) = HVectElim ts a -> HVect ts -> a
forall (ts :: [*]) a. HVectElim ts a -> HVect ts -> a
uncurry (HVectElim ts a
t -> HVectElim ts a
f t
x) HVect ts
xs

data Rep (ts :: [*]) where
  RNil :: Rep '[]
  RCons :: Rep ts -> Rep (t ': ts)

class HasRep (ts :: [*]) where
  hasRep :: Rep ts

instance HasRep '[] where
  hasRep :: Rep '[]
hasRep = Rep '[]
RNil

instance HasRep ts => HasRep (t ': ts) where
  hasRep :: Rep (t : ts)
hasRep = Rep ts -> Rep (t : ts)
forall (ts :: [*]) t. Rep ts -> Rep (t : ts)
RCons Rep ts
forall (ts :: [*]). HasRep ts => Rep ts
hasRep

curryExpl :: Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl :: Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl Rep ts
RNil HVect ts -> a
f = HVect ts -> a
f HVect ts
HVect '[]
HNil
curryExpl (RCons Rep ts
r) HVect ts -> a
f = \t
x -> Rep ts -> (HVect ts -> a) -> HVectElim ts a
forall (ts :: [*]) a. Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl Rep ts
r (HVect ts -> a
f (HVect ts -> a) -> (HVect ts -> HVect ts) -> HVect ts -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> HVect ts -> HVect (t : ts)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
(:&:) t
x)

curry :: HasRep ts => (HVect ts -> a) -> HVectElim ts a
curry :: (HVect ts -> a) -> HVectElim ts a
curry = Rep ts -> (HVect ts -> a) -> HVectElim ts a
forall (ts :: [*]) a. Rep ts -> (HVect ts -> a) -> HVectElim ts a
curryExpl Rep ts
forall (ts :: [*]). HasRep ts => Rep ts
hasRep

buildElim :: Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim :: Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim Rep ts
RNil HVect ts -> HVect ss
f = HVect ts -> HVect ss
f HVect ts
HVect '[]
HNil
buildElim (RCons Rep ts
r) HVect ts -> HVect ss
f = \t
x -> Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
forall (ts :: [*]) (ss :: [*]).
Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim Rep ts
r (HVect ts -> HVect ss
f (HVect ts -> HVect ss)
-> (HVect ts -> HVect ts) -> HVect ts -> HVect ss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> HVect ts -> HVect (t : ts)
forall t (ts :: [*]). t -> HVect ts -> HVect (t : ts)
(:&:) t
x)

packExpl :: Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
packExpl :: Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
packExpl Rep ts
rep forall a. HVectElim ts a -> a
f = HVectElim ts (HVect ts) -> HVect ts
forall a. HVectElim ts a -> a
f (Rep ts -> (HVect ts -> HVect ts) -> HVectElim ts (HVect ts)
forall (ts :: [*]) (ss :: [*]).
Rep ts -> (HVect ts -> HVect ss) -> HVectElim ts (HVect ss)
buildElim Rep ts
rep HVect ts -> HVect ts
forall a. a -> a
id)

pack :: HasRep ts => (forall a. HVectElim ts a -> a) -> HVect ts
pack :: (forall a. HVectElim ts a -> a) -> HVect ts
pack = Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
forall (ts :: [*]).
Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts
packExpl Rep ts
forall (ts :: [*]). HasRep ts => Rep ts
hasRep