{-# LANGUAGE UndecidableInstances, ScopedTypeVariables, EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
--
-- .$Header: c:/Source/Haskell/Combine/Control/RCS/Combine.hs,v 1.7 2011/09/14 02:00:34 dosuser Exp dosuser $
module Control.Combine where

import Data.Type.Apply
import Data.Type.Eq
import Data.Type.Nat

class ComposeType n a b c | n a b -> c

instance (TypeCast d a, TypeCast e c, TypeCast f b) =>
    ComposeType Z (b -> c) (a -> f) (d -> e)

instance ComposeType n (b -> c) s t =>
    ComposeType (S n) (b -> c) (a -> s) (a -> t)

data C f g

instance Apply (C (b -> c) (a -> b)) Z ((b -> c) -> (a -> b) -> (a -> c)) where
    apply _ _ = (.)

instance forall n a b c s t. Apply (C (b -> c) s) n ((b -> c) -> s -> t) =>
    Apply (C (b -> c) (a -> s)) (S n) ((b -> c) -> (a -> s) -> (a -> t))
  where
    apply _ _ = (.) . apply (undefined :: C (b -> c) s) (undefined :: n)

-- Extended function composition e.g.
-- compose zero = (.)
-- compose zero f g x = f (g x)
-- compose one f g x y = f (g x y)

class Compose n a b c | n a b -> c where
    compose :: n -> a -> b -> c

instance forall n a b c d e f. (ComposeType n (b -> c) (a -> f) (d -> e),
        Apply (C (b -> c) (a -> f)) n ((b -> c) -> (a -> f) -> (d -> e))
    ) =>
    Compose n (b -> c) (a -> f) (d -> e)
  where
    compose _ = apply (undefined :: C (b -> c) (a -> f)) (undefined :: n)

class FlipType n a b | n a -> b

instance (TypeCast d a, TypeCast e b, TypeCast f c) =>
    FlipType Z (a -> b -> c) ((d -> e -> f) -> (e -> d -> f))

instance
    FlipType n f ((a -> b -> c -> d) -> (b -> a -> c -> d)) =>
    FlipType (S n) f ((b -> c -> d) -> (c -> b -> d))

class RotType n a b | n a -> b

instance TypeCast a b => RotType Z a b
instance (TypeCast d b, TypeCast e a, TypeCast f c) =>
    RotType (S Z) (a -> b -> c) (d -> e -> f)
instance (RotType (S n) b g,
        FlipType (S n) a ((d -> e -> f) -> (e -> d -> f)),
        ComposeType n ((d -> e -> f) -> (e -> d -> f)) a b
    ) =>
    RotType (S (S n)) a g

data R a

instance Apply (R a) Z (a -> a) where
    apply _ _ = id
instance Apply (R (b -> a -> c)) (S Z) ((b -> a -> c) -> (a -> b -> c)) where
    apply _ _ = flip
instance forall n a b c d e f. (Apply (R b) (S n) (b -> f),
        FlipType (S n) a ((c -> d -> e) -> (d -> c -> e)),
        Compose n ((c -> d -> e) -> (d -> c -> e)) a b
    ) =>
        Apply (R a) (S (S n)) (a -> f) where
    apply _ _ =
        apply (undefined :: R b) (undefined :: S n) .
            compose (undefined :: n) (flip :: ((c -> d -> e) -> (d -> c -> e)))

-- <rot n f> passes its first argument as the (n + 1)th argument
-- to <f>, rotating the intervening arguments along
-- e.g. <rot one> = flip

class Rot n a b | n a -> b where
    rot :: n -> a -> b

instance forall n a b. (
        RotType n a b,
        Apply (R a) n (a -> b)
    ) =>
        Rot n a b where
    rot _ = apply (undefined :: R a) (undefined :: n)

-- vim: expandtab:tabstop=4:shiftwidth=4