{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{- |
This is an example of using constraints-deriving plugin for optimization.
This module presents a "front-end" Vector data type visible to a user.
It is a simple newtype wrapper over a "backend" data type family.
Behind the scenes, the compiler chooses the most efficient representations
for the backend based on a type family `Backend t n`.
For example, if the compiler knows that the size of a vector is 1,
than the `Vector t 1` type is a newtype wrapper over `t`,
and GHC statically uses all type class instances for `t`, sidestepping dynamic instance elaboration.
But, if GHC does not know the dimensionality of the vector statically,
it selects class instances dynamically at runtime.
-}
module Lib.Vector
( -- * Data types
Vector (Z, (:*))
, SomeVector (..), KnownBackend (), Backend
, Nat
) where
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif
import Data.Constraint
import GHC.Base (Type, unsafeCoerce#)
import GHC.TypeLits (type (+), type (-), KnownNat, Nat)
import Lib.BackendFamily
import Lib.VecBackend
newtype Vector (t :: Type) (n ::Nat) = Vector (VecBackend t n (Backend t n))
pattern Z :: forall t n
. KnownBackend (Vector t n)
=> n ~ 0
=> Vector t n
pattern Z <- (vUncons -> Left Dict)
where
Z = Vector (VecBackend bNil)
pattern (:*) :: forall t n
. KnownBackend (Vector t n)
=> forall m
. (KnownBackend (Vector t m), n ~ (m + 1), m ~ (n - 1))
=> t -> Vector t m -> Vector t n
pattern (:*) x xs <- (vUncons -> Right (Dict, x, xs))
where
(:*) = vCons
infixr 7 :*
#if __GLASGOW_HASKELL__ >= 802
{-# Complete Z, (:*) #-}
#endif
vUncons :: forall t n m
. KnownBackend (Vector t n)
=> Vector t n
-> Either ( Dict ( n ~ 0
, n ~ DataDims (Vector t n)
, t ~ DataElemType (Vector t n)
))
( Dict ( KnownBackend (Vector t m)
, n ~ (m + 1)
, m ~ (n - 1)
, n ~ DataDims (Vector t n)
, m ~ DataDims (Vector t m)
, t ~ DataElemType (Vector t n)
, t ~ DataElemType (Vector t m)
)
, t, Vector t m )
vUncons = case underiveKB @t @n of Dict -> unsafeCoerce# (bUncons @t @n @m)
vCons :: forall t n
. KnownBackend (Vector t n)
=> t -> Vector t n -> Vector t (n + 1)
vCons = case underiveKB @t @n of Dict -> unsafeCoerce# (bCons @t @n)
data SomeVector (t :: Type) where
SomeVector :: (KnownNat (n :: Nat), KnownBackend (Backend t n))
=> Vector t n -> SomeVector t
type instance DataElemType (Vector t n) = t
type instance DataDims (Vector t n) = n
instance (KnownBackend (Vector t n), Show t) => Show (Vector t n) where
show Z = "Z"
show (x :* xs) = show x ++ " :* " ++ show xs
instance KnownBackend (Backend t n) => KnownBackend (Vector t n)
deriving instance Eq (VecBackend t n (Backend t n)) => Eq (Vector t n)
deriving instance Ord (VecBackend t n (Backend t n)) => Ord (Vector t n)
deriving instance Semigroup (VecBackend t n (Backend t n)) => Semigroup (Vector t n)
deriving instance Monoid (VecBackend t n (Backend t n)) => Monoid (Vector t n)
underiveKB :: forall t n . KnownBackend (Vector t n) => Dict (KnownBackend (Backend t n))
underiveKB = unsafeCoerce# (Dict @(KnownBackend (Vector t n)))