HVect.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

module HVect where

import GHC.Exts (Constraint)
import Prelude hiding (zip)
import Data.Monoid ((<>))
import Data.List (intercalate)

data HVect (ts :: [*]) where
  HNil :: HVect '[]
  HCons :: t -> HVect ts -> HVect (t ': ts)

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

(<++>) :: HVect as -> HVect bs -> HVect (as ++ bs)
HNil <++> bs = bs
(HCons a as) <++> bs = HCons a (as <++> bs)

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

hVectUncurry :: HVectElim ts a -> HVect ts -> a
hVectUncurry f HNil = f
hVectUncurry f (HCons x xs) = hVectUncurry (f x) xs

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

getRep :: HVect ts -> Rep ts
getRep HNil = RNil
getRep (HCons _ xs) = RCons (getRep xs)

hVectCurryExpl :: Rep ts -> (HVect ts -> a) -> HVectElim ts a
hVectCurryExpl RNil f = f HNil
hVectCurryExpl (RCons r) f = \x -> hVectCurryExpl r (f . HCons x)

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

instance HasRep '[] where
  hasRep = RNil

instance HasRep ts => HasRep (t ': ts) where
  hasRep = RCons hasRep

hVectCurry :: HasRep ts => (HVect ts -> a) -> HVectElim ts a
hVectCurry = hVectCurryExpl hasRep

type family RecAll (ts :: [*]) (c :: * -> Constraint) :: Constraint
type instance RecAll '[] c = ()
type instance RecAll (t ': ts) c = (c t, RecAll ts c)

instance RecAll ts Show => Show (HVect ts) where
  show HNil = "HNil"
  show (HCons a as) = "HVect (" ++ show a ++ ") (" ++ show as ++ ")"

data Dict (c :: * -> Constraint) a where
  Dict :: c a => a -> Dict c a

type family Map (f :: * -> *) (ts :: [*]) :: [*] where
  Map f '[] = '[]
  Map f (t ': ts) = f t ': Map f ts

reifyConstraints :: RecAll ts c => proxy c -> HVect ts -> HVect (Map (Dict c) ts)
reifyConstraints _prx HNil = HNil
reifyConstraints prx (HCons a as) = HCons (Dict a) (reifyConstraints prx as)

vmapExpl :: Rep tss -> (forall a. f a -> g a) -> HVect (Map f tss) -> HVect (Map g tss)
vmapExpl RNil f HNil = HNil
vmapExpl (RCons r) f (HCons x xs) = HCons (f x) (vmapExpl r f xs)

vmap :: HasRep tss => proxy tss -> (forall a. f a -> g a) -> HVect (Map f tss) -> HVect (Map g tss)
vmap (prx :: proxy tss) = vmapExpl (hasRep :: Rep tss)

mapConstExpl :: Rep tss -> (forall a. f a -> b) -> HVect (Map f tss) -> [b]
mapConstExpl RNil f HNil = []
mapConstExpl (RCons rs) f (HCons x xs) = f x : mapConstExpl rs f xs

mapConst :: HasRep tss => proxy tss -> (forall a. f a -> b) -> HVect (Map f tss) -> [b]
mapConst (prx :: proxy tss) = mapConstExpl (hasRep :: Rep tss)

toTuple2 :: HVect '[a,b] -> (a, b)
toTuple2 (HCons a (HCons b HNil)) = (a, b)

fromTuple2 :: (a, b) -> HVect '[a,b]
fromTuple2 (a, b) = HCons a (HCons b HNil)

toTuple3 :: HVect '[a,b,c] -> (a, b, c)
toTuple3 (HCons a (HCons b (HCons c HNil))) = (a, b, c)

fromTuple3 :: (a, b, c) -> HVect '[a,b,c]
fromTuple3 (a, b, c) = HCons a (HCons b (HCons c HNil))

type family HomogeneousT a (ts :: [*]) :: Constraint
type instance HomogeneousT a '[] = ()
type instance HomogeneousT a (t ': ts) = (a ~ t, HomogeneousT a ts)

type family Homogeneous (ts :: [*]) :: Constraint
type instance Homogeneous '[] = ()
type instance Homogeneous (t ': ts) = HomogeneousT t ts

toList :: HomogeneousT a ts => HVect ts -> [a]
toList HNil = []
toList (HCons a as) = a : toList as

type family Nested (ass :: [[*]]) :: [*]
type instance Nested '[] = '[]
type instance Nested (ts ': tss) = HVect ts ': Nested tss

type family Flatten (ass :: [[*]]) :: [*]
type instance Flatten '[] = '[]
type instance Flatten (ts ': tss) = ts ++ Flatten tss

flattenExpl :: Rep tss -> HVect (Nested tss) -> HVect (Flatten tss)
flattenExpl RNil HNil = HNil
flattenExpl (RCons rep) (HCons as ass) = as <++> flattenExpl rep ass

flatten :: HasRep tss => proxy tss -> HVect (Nested tss) -> HVect (Flatten tss)
flatten (_prx :: proxy tss) = flattenExpl (hasRep :: Rep tss)

data Proxy :: k -> * where
  Proxy :: Proxy k

showAll :: (RecAll ts Show, HasRep ts) => HVect ts -> String
showAll xs =
  (\str -> "{" <> str <> "}")
    . intercalate ", "
    . mapConstExpl (getRep xs) (\(Dict x :: Dict Show a) -> show x)
    $ reifyConstraints (Proxy :: Proxy Show) xs