{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeFamilies #-}
{- |
Module: Data.Prodder
Copyright: (c) Samuel Schlesinger 2020
License: MIT
Maintainer: sgschlesinger@gmail.com
Stability: experimental
Portability: non-portable
Description: Extensible products
-}
module Data.Prodder
  ( -- * The extensible product type
    Prod
    -- * Construction and deconstruction
  , extract
  , index
  , tailN
  , initN
  , dropFirst
  , Consume(consume, produce, extend1, cmap)
    -- * Type families
  , IndexIn
  , HasIndexIn
  , Consumer
  , type (<>)
  , Length
  , Tail
  , Init
  , Replace
    -- * Rearranging and removing elements
  , Strengthen(strengthen)
    -- * Transforming extensible products
  , remap
  ) where

import Control.Monad (unless)
import Control.Exception (catch, SomeException)
import GHC.Exts (Any)
import Unsafe.Coerce (unsafeCoerce)
import Data.Vector (Vector)
import qualified Data.Vector as V
import GHC.TypeLits (KnownNat, type (+), type (-), natVal, type (<=))
import Data.Proxy (Proxy(Proxy))

-- | An extensible product type
data Prod (xs :: [*]) = UnsafeProd { Prod xs -> Vector Any
unProd :: Vector Any }

type role Prod representational

-- | A type family for computing the index of a type in a list of types.
type family IndexIn (x :: k) (xs :: [k]) where
  IndexIn x (x ': xs) = 0
  IndexIn x (y ': xs) = 1 + IndexIn x xs

-- | A type family for computing the length of a type level list
type family Length (xs :: [k]) where
  Length '[] = 0
  Length (x ': xs) = 1 + Length xs

-- | A type family for computing the tail of a type level list
type family Tail n xs where
  Tail 0 xs = xs
  Tail n (x ': xs) = Tail (n - 1) xs

-- | A type family for computing the initial segment of a type level list
type family Init n xs where
  Init 0 xs = '[]
  Init n (x ': xs) = x ': Init (n - 1) xs

-- | A class that is used for convenience in order to make certain type
-- signatures read more clearly.
class KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs
instance KnownNat (x `IndexIn` xs) => x `HasIndexIn` xs

-- | Computes the index of the given type in the given type level list.
index :: forall x xs. x `HasIndexIn` xs => Word
index :: Word
index = Integer -> Word
forall a. Num a => Integer -> a
fromInteger (Integer -> Word) -> Integer -> Word
forall a b. (a -> b) -> a -> b
$ Proxy (IndexIn x xs) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (IndexIn x xs)
forall k (t :: k). Proxy t
Proxy @(IndexIn x xs))
{-# INLINE CONLIKE index #-}

-- | Extract a value at a particular index
extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x
extract :: Prod xs -> x
extract (UnsafeProd Vector Any
v) = Any -> x
forall a b. a -> b
unsafeCoerce (Any -> x) -> Any -> x
forall a b. (a -> b) -> a -> b
$ Vector Any
v Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (HasIndexIn x xs => Word
forall k (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index @x @xs)
{-# INLINE CONLIKE extract #-}

-- | Takes the tail of a product after the nth element.
tailN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Tail n xs)
tailN :: Prod xs -> Prod (Tail n xs)
tailN (UnsafeProd Vector Any
v) = Vector Any -> Prod (Tail n xs)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod (Tail n xs)) -> Vector Any -> Prod (Tail n xs)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Any -> Vector Any
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
n (Vector Any -> Int
forall a. Vector a -> Int
V.length Vector Any
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) Vector Any
v
  where
    n :: Int
n = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
{-# INLINE CONLIKE tailN #-}

-- | Takes the initial length n segment of a product.
initN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Init n xs)
initN :: Prod xs -> Prod (Init n xs)
initN (UnsafeProd Vector Any
v) = Vector Any -> Prod (Init n xs)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod (Init n xs)) -> Vector Any -> Prod (Init n xs)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Any -> Vector Any
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
0 Int
n Vector Any
v
  where
    n :: Int
n = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
{-# INLINE CONLIKE initN #-}

-- | Drop the first element of a product. Sometimes needed for better type
-- inference and less piping around of constraints.
dropFirst :: forall x xs. Prod (x ': xs) -> Prod xs
dropFirst :: Prod (x : xs) -> Prod xs
dropFirst (UnsafeProd Vector Any
v) = Vector Any -> Prod xs
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod xs) -> Vector Any -> Prod xs
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Any -> Vector Any
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
1 (Vector Any -> Int
forall a. Vector a -> Int
V.length Vector Any
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Vector Any
v


type family (<>) (xs :: [k]) (ys :: [k]) :: [k] where
  '[] <> ys = ys
  (x ': xs) <> ys = x ': (xs <> ys)
combine :: forall xs ys. Prod xs -> Prod ys -> Prod (xs <> ys)
combine :: Prod xs -> Prod ys -> Prod (xs <> ys)
combine (UnsafeProd Vector Any
p) (UnsafeProd Vector Any
q) = Vector Any -> Prod (xs <> ys)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any
p Vector Any -> Vector Any -> Vector Any
forall a. Vector a -> Vector a -> Vector a
V.++ Vector Any
q)
{-# INLINE CONLIKE combine #-}

-- | Type family for replacing one type in a type level list with another
type family Replace x y xs where
  Replace x y (x ': xs) = y ': xs
  Replace x y (z ': xs) = z ': Replace x y xs

-- | Replaces one type with another via a function
remap :: forall x y xs. x `HasIndexIn` xs => (x -> y) -> Prod xs -> Prod (Replace x y xs)
remap :: (x -> y) -> Prod xs -> Prod (Replace x y xs)
remap x -> y
f (UnsafeProd Vector Any
v) = Vector Any -> Prod (Replace x y xs)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Int -> Any -> Any
update (Int -> Any -> Any) -> Vector Any -> Vector Any
forall a b. (Int -> a -> b) -> Vector a -> Vector b
`V.imap` Vector Any
v) where
  update :: Int -> Any -> Any
  update :: Int -> Any -> Any
update (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral -> Word
n) Any
a
    | Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasIndexIn x xs => Word
forall k (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index @x @xs = y -> Any
forall a b. a -> b
unsafeCoerce (y -> Any) -> y -> Any
forall a b. (a -> b) -> a -> b
$ x -> y
f (x -> y) -> x -> y
forall a b. (a -> b) -> a -> b
$ Any -> x
forall a b. a -> b
unsafeCoerce Any
a
    | Bool
otherwise = Any
a
  {-# INLINE CONLIKE update #-}
{-# INLINE CONLIKE remap #-}

-- | This is a reified pattern match on an extensible product
type family Consumer xs r where
  Consumer '[] r = r
  Consumer (x ': xs) r = x -> Consumer xs r

-- | A typeclass that is useful to define the scott encoding/decoding for
-- extensible products.
class Consume xs where
  consume :: forall r. Prod xs -> Consumer xs r -> r
  produce :: (forall r. Consumer xs r -> r) -> Prod xs
  extend1 :: x -> Consumer xs (Prod (x ': xs))
  cmap :: (r -> r') -> Consumer xs r -> Consumer xs r' 

instance Consume '[] where
  consume :: Prod '[] -> Consumer '[] r -> r
consume = (r -> Prod '[] -> r) -> Prod '[] -> r -> r
forall a b c. (a -> b -> c) -> b -> a -> c
flip r -> Prod '[] -> r
forall a b. a -> b -> a
const
  {-# INLINE CONLIKE consume #-}
  produce :: (forall r. Consumer '[] r -> r) -> Prod '[]
produce forall r. Consumer '[] r -> r
x = Vector Any -> Prod '[]
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd Vector Any
forall a. Vector a
V.empty
  {-# INLINE CONLIKE produce #-}
  extend1 :: x -> Consumer '[] (Prod '[x])
extend1 x
x = Vector Any -> Prod '[x]
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Any -> Vector Any
forall a. a -> Vector a
V.singleton (x -> Any
forall a b. a -> b
unsafeCoerce x
x))
  {-# INLINE CONLIKE extend1 #-}
  cmap :: (r -> r') -> Consumer '[] r -> Consumer '[] r'
cmap r -> r'
f Consumer '[] r
x = r -> r'
f r
Consumer '[] r
x
  {-# INLINE CONLIKE cmap #-}

instance Consume xs => Consume (x ': xs) where
  consume :: Prod (x : xs) -> Consumer (x : xs) r -> r
consume (UnsafeProd Vector Any
v) Consumer (x : xs) r
g = Prod xs -> Consumer xs r -> r
forall (xs :: [*]) r. Consume xs => Prod xs -> Consumer xs r -> r
consume @xs (Vector Any -> Prod xs
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Vector Any
forall a. Vector a -> Vector a
V.tail Vector Any
v)) (Consumer xs r -> r) -> Consumer xs r -> r
forall a b. (a -> b) -> a -> b
$ Consumer (x : xs) r
x -> Consumer xs r
g (Any -> x
forall a b. a -> b
unsafeCoerce (Any -> x) -> Any -> x
forall a b. (a -> b) -> a -> b
$ Vector Any
v Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Int
0)
  {-# INLINE CONLIKE consume #-}
  produce :: (forall r. Consumer (x : xs) r -> r) -> Prod (x : xs)
produce forall r. Consumer (x : xs) r -> r
g = Consumer (x : xs) (Prod (x : xs)) -> Prod (x : xs)
forall r. Consumer (x : xs) r -> r
g (forall x. Consume xs => x -> Consumer xs (Prod (x : xs))
forall (xs :: [*]) x.
Consume xs =>
x -> Consumer xs (Prod (x : xs))
extend1 @xs)
  {-# INLINE CONLIKE produce #-}
  cmap :: (r -> r') -> Consumer (x : xs) r -> Consumer (x : xs) r'
cmap r -> r'
f = (Consumer xs r -> Consumer xs r')
-> (x -> Consumer xs r) -> x -> Consumer xs r'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((r -> r') -> Consumer xs r -> Consumer xs r'
forall (xs :: [*]) r r'.
Consume xs =>
(r -> r') -> Consumer xs r -> Consumer xs r'
cmap @xs r -> r'
f)
  {-# INLINE CONLIKE cmap #-}
  extend1 :: x -> Consumer (x : xs) (Prod (x : x : xs))
extend1 (x
x1 :: x1) x
x = (Prod (x : xs) -> Prod (x : x : xs))
-> Consumer xs (Prod (x : xs)) -> Consumer xs (Prod (x : x : xs))
forall (xs :: [*]) r r'.
Consume xs =>
(r -> r') -> Consumer xs r -> Consumer xs r'
cmap @xs @(Prod (x ': xs)) @(Prod (x1 ': x ': xs)) (Vector Any -> Prod (x : x : xs)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod (x : x : xs))
-> (Prod (x : xs) -> Vector Any)
-> Prod (x : xs)
-> Prod (x : x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Any -> Vector Any
forall a. a -> Vector a
V.singleton (x -> Any
forall a b. a -> b
unsafeCoerce x
x1) Vector Any -> Vector Any -> Vector Any
forall a. Vector a -> Vector a -> Vector a
V.++) (Vector Any -> Vector Any)
-> (Prod (x : xs) -> Vector Any) -> Prod (x : xs) -> Vector Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prod (x : xs) -> Vector Any
forall (xs :: [*]). Prod xs -> Vector Any
unProd) (x -> Consumer xs (Prod (x : xs))
forall (xs :: [*]) x.
Consume xs =>
x -> Consumer xs (Prod (x : xs))
extend1 @xs x
x)
  {-# INLINE CONLIKE extend1 #-}

instance Eq (Prod '[]) where
  Prod '[]
_ == :: Prod '[] -> Prod '[] -> Bool
== Prod '[]
_ = Bool
True
  {-# INLINE CONLIKE (==) #-}

instance (Eq x, Eq (Prod xs)) => Eq (Prod (x ': xs)) where
  px :: Prod (x : xs)
px@(UnsafeProd Vector Any
x) == :: Prod (x : xs) -> Prod (x : xs) -> Bool
== py :: Prod (x : xs)
py@(UnsafeProd Vector Any
y) = Any -> x
forall a b. a -> b
unsafeCoerce @_ @x (Vector Any
x Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Int
0) x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== Any -> x
forall a b. a -> b
unsafeCoerce @_ @x (Vector Any
y Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Int
0) Bool -> Bool -> Bool
&& Prod (x : xs) -> Prod xs
forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
px Prod xs -> Prod xs -> Bool
forall a. Eq a => a -> a -> Bool
== Prod (x : xs) -> Prod xs
forall x (xs :: [*]). Prod (x : xs) -> Prod xs
dropFirst Prod (x : xs)
py
  {-# INLINE CONLIKE (==) #-}

-- | A typeclass to rearrange and possibly remove things from a product.
class Strengthen xs ys where
  strengthen :: Prod xs -> Prod ys
instance (Strengthen xs ys, y `HasIndexIn` xs) => Strengthen xs (y ': ys) where
  strengthen :: Prod xs -> Prod (y : ys)
strengthen Prod xs
p = Vector Any -> Prod (y : ys)
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd (Vector Any -> Prod (y : ys)) -> Vector Any -> Prod (y : ys)
forall a b. (a -> b) -> a -> b
$ Any -> Vector Any
forall a. a -> Vector a
V.singleton (Any -> Any
forall a b. a -> b
unsafeCoerce (Any -> Any) -> Any -> Any
forall a b. (a -> b) -> a -> b
$ Prod xs -> Vector Any
forall (xs :: [*]). Prod xs -> Vector Any
unProd Prod xs
p Vector Any -> Int -> Any
forall a. Vector a -> Int -> a
V.! Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (HasIndexIn y xs => Word
forall k (x :: k) (xs :: [k]). HasIndexIn x xs => Word
index @y @xs)) Vector Any -> Vector Any -> Vector Any
forall a. Semigroup a => a -> a -> a
<> Prod ys -> Vector Any
forall (xs :: [*]). Prod xs -> Vector Any
unProd (Prod xs -> Prod ys
forall (xs :: [*]) (ys :: [*]).
Strengthen xs ys =>
Prod xs -> Prod ys
strengthen @xs @ys Prod xs
p)
  {-# INLINE CONLIKE strengthen #-}
instance Strengthen xs '[] where
  strengthen :: Prod xs -> Prod '[]
strengthen = Prod '[] -> Prod xs -> Prod '[]
forall a b. a -> b -> a
const (Vector Any -> Prod '[]
forall (xs :: [*]). Vector Any -> Prod xs
UnsafeProd Vector Any
forall a. Vector a
V.empty)
  {-# INLINE CONLIKE strengthen #-}