{-# Language DataKinds ,AllowAmbiguousTypes,FunctionalDependencies, RankNTypes,TypeOperators ,ScopedTypeVariables, TypeFamilies , TypeFamilyDependencies , KindSignatures , GADTs , TypeApplications , FlexibleInstances , StandaloneDeriving , MultiParamTypeClasses , FlexibleContexts , UndecidableInstances , ConstraintKinds #-}
import Data.Proxy
import Data.Kind
class Stateful s i o | s -> i , s -> o where
stateFunction :: s -> i -> (s,o)
---
-- Lag
data Lag = Lag Double Double deriving (Read,Show)
instance Stateful Lag Double Double where
stateFunction (Lag la b) i = (Lag la o,o)
where
o = b * x + i * y
x = la ** 0.01
y = (1-x)
egLag :: Lag
egLag = Lag 0.5 0
---
-- Extend
data Extend = Extend Lag deriving (Read,Show)
instance Stateful Extend Double Double where
stateFunction (Extend l) i = (Extend l',o)
where
(l',x) = stateFunction l i
o = 2*i-x
egExtend :: Extend
egExtend = Extend $ Lag 0.5 0
---
-- Nat
data Nat = S Nat | Z
-- Type-level addition
type family Plus (x :: Nat) (y :: Nat) :: Nat where
Plus Z y = y
Plus (S x) y = S (Plus x y)
proxyPlus :: Proxy (n::Nat) -> Proxy (m::Nat) -> Proxy(Plus n m)
proxyPlus _ _ = Proxy
-- Value-level conversion for Nat
class FromNat (n :: Nat) where
fromNat :: Int
instance FromNat Z where
fromNat = 0
instance FromNat n => FromNat (S n) where
fromNat = 1 + fromNat @n
---
-- Nonempty
data Nonempty a = Cons a (Nonempty a) | Last a
type family Length (xs :: Nonempty Type) :: Nat where
Length ('Last x) = (S Z)
Length ('Cons x xs) = S (Length xs)
---
-- Transfers
data Transfers (xs :: Nonempty *) where
ConsTransfers :: x -> Transfers xs -> Transfers (Cons x xs)
LastTransfer :: x -> Transfers (Last x)
instance (Stateful x i o,Stateful (Transfers xs) [i] [o]) => Stateful (Transfers (Cons x xs)) [i] [o] where
stateFunction (ConsTransfers x xs) (i:is) = let ((x',o),(xs',os)) = (stateFunction x i,stateFunction xs is) in (ConsTransfers x' xs',(:) o os)
instance Stateful x i o => Stateful (Transfers (Last x)) [i] [o] where
stateFunction (LastTransfer x) [i] = let (x',o) = stateFunction x i in (LastTransfer x',[o])
deProxy :: forall n. FromNat n => Proxy (n::Nat) -> Int
deProxy _ = fromNat @n
class TransfersLength (xs :: Nonempty *) where
transfersLength :: Transfers xs -> Proxy (Length xs)
instance TransfersLength (Last a) where
transfersLength _ = Proxy @(S Z)
instance TransfersLength xs => TransfersLength (Cons x xs) where
transfersLength (ConsTransfers _ xs) = proxyPlus (Proxy @(S Z)) (transfersLength xs)
transfers :: (TransfersLength xs,FromNat n,n~(Length xs),Stateful (Transfers xs) [i] [o]) => Transfers xs -> i -> (Transfers xs,[o])
transfers ts i = stateFunction ts (replicate l i)
where
l = deProxy $ transfersLength ts
type Disp x = (Read x,Show x)
instance (Disp x) => Show (Transfers (Last x)) where
show (LastTransfer x) = show x
-- readsPrec :: String -> [(a, String)]
instance (Disp x) => Read (Transfers (Last x)) where
readsPrec n str = let [(a,b)] = readsPrec n str in [(LastTransfer a,b)]
instance (Disp x,Disp (Transfers xs)) => Show (Transfers (Cons x xs)) where
show (ConsTransfers x xs) = show (x,xs)
instance (Disp x,Disp (Transfers xs)) => Read (Transfers (Cons x xs)) where
readsPrec n str = let [((x,xs),b)] = readsPrec n str in [(ConsTransfers x xs,b)]
egTransfers :: Transfers (Cons Lag (Last Extend))
egTransfers = ConsTransfers egLag (LastTransfer egExtend)
test :: IO ()
test = do
let f = egTransfers
let (f',o) = transfers f 1
print f
print f'
print o
main = test