{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Vector.HFixed.TypeFuns (
Proxy(..)
, proxy
, type (++)
, Len
, HomList
) where
import Data.Typeable (Proxy(..))
import Data.Vector.Fixed.Cont (PeanoNum(..))
proxy :: t -> Proxy t
proxy :: t -> Proxy t
proxy t
_ = Proxy t
forall k (t :: k). Proxy t
Proxy
type family (++) (xs :: [α]) (ys :: [α]) :: [α] where
(++) '[] ys = ys
(++) (x : xs) ys = x : xs ++ ys
type family Len (xs :: [α]) :: PeanoNum where
Len '[] = 'Z
Len (x : xs) = 'S (Len xs)
type family HomList (n :: PeanoNum) (a :: α) :: [α] where
HomList 'Z a = '[]
HomList ('S n) a = a : HomList n a