OverloadedDo exploration

OverloadedDo.hs

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE DeriveDataTypeable #-}

module Main where

import Prelude
import qualified Prelude as P

import GHC.TypeLits
import Data.Proxy
import Data.Kind
import Data.Type.Bool
import Data.Typeable

import Sized



data ApplicativeDoableDict f
    = ApplicativeF (forall a f . Applicative f => a -> f a) (forall f a b . Applicative f => f (a -> b) -> f a -> f b)
    | SizedApplicativeF (forall a f . SizedApplicative f => a -> f 0 a) (forall f a b k i j . (SizedApplicative f, k ~ Max i j) => f i (a -> b) -> f j a -> f k b)
    deriving (Typeable)

data DoableDict m
  = Monadic (ApplicativeDoableDict m) (forall m a b . Monad m => m a -> (a -> m b) -> m b)
  | SizedMonadic (ApplicativeDoableDict m) (forall m a b i j . SizedMonad m => m i a -> (a -> m j b) -> m (i+j) b)
    deriving (Typeable)

class ApplicativeDoable f where
  adoDict :: ApplicativeDoableDict f

class  ApplicativeDoable m => Doable m where
  doDict :: DoableDict m

instance {-# OVERLAPPABLE #-} Applicative f => ApplicativeDoable f where
  adoDict = ApplicativeF P.pure (P.<*>)

instance {-# OVERLAPPABLE #-} (Typeable m, Monad m) => Doable m where
 doDict = Monadic adoDict (P.>>=)

instance {-# OVERLAPPING #-} SizedApplicative f => ApplicativeDoable (f (n :: Nat)) where
  adoDict = SizedApplicativeF spure (|<*>)

instance {-# OVERLAPPING #-} (Typeable (f n), SizedMonad f) => Doable (f (n :: Nat)) where
  doDict = SizedMonadic adoDict (|>>=)

one :: () -> SizedIO 1 ()
one _ = wrapWithCost (Proxy :: Proxy 1) $ putStrLn "one"

two :: () -> SizedT IO 2 ()
two _ = wrapWithCost (Proxy :: Proxy 2) $ putStrLn "two"

three :: () -> SizedIO 3 ()
three _ = wrapWithCost (Proxy :: Proxy 3) $ putStrLn "three"

t0a :: SizedIO 6 ()
t0a = do { x <- one ()
         ; y <- two x
         ; z <- three y
         ; () |<$ return (x,y,z)}
    where dd = doDict :: DoableDict (SizedIO 6)
          SizedMonadic (SizedApplicativeF return (<*>)) (>>=) = dd

t2 :: IO ()
t2 = do { x <- putStrLn "hey"
        ; print x }
     where dd = doDict :: DoableDict IO
           Monadic (ApplicativeF return (<*>)) (>>=) = dd

main :: IO ()
main = do { t2
          ; runSizedT t0a }

Sized.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Sized where

import GHC.TypeLits
import Data.Type.Bool
import Data.Proxy
import Data.Type.Equality
import Debug.Trace

-- Type level Maximum function
type family Max (a :: Nat) (b :: Nat) :: Nat where
  Max a 0 = a
  Max 0 b = b
  Max a b = If (a <=? b) b a


class SizedFunctor f where
  sfmap :: (a -> b) -> f i a -> f i b
  (|<$) :: a -> f i b -> f i a
  (|<$) = sfmap . const

(|<$>) :: (SizedFunctor f) => (a -> b) -> f i a -> f i b
f |<$> b = sfmap f b

class (SizedFunctor f) => SizedApplicative f where
  spure :: a -> f 0 a
  (|<*>) ::  (k ~ Max i j) => f i (a -> b) -> f j a -> f k b

  -- You can only sequence free stuff
  -- This type is a bit weird, but without it (and then defining
  -- (>>) as (|*>)), you get a lot of ambigous type variables from
  -- ApplicativeDo.
  (|*>) :: f i a -> f 0 b -> f i b
  a |*> b = (id |<$ a) |<*> b

class SizedApplicative m  => SizedMonad m  where
  (|>>=) ::  m i a -> (a -> m j b) -> m (i + j)  b

  sreturn :: a -> m 0 a
  sreturn = spure

  join :: m i (m j a) -> m (i + j)  a
  join m = m |>>= id

  -- This should never be used, since
  -- we never want to sequence without dependencies
  -- those should only be done with appliatives.
  -- but we have this here to allow explicit forcing of sequencing
  -- Use (*>) to express sequencing.
  (|>>) :: m i a -> m j b -> m (i+j) b
  a |>> b = a |>>= (\_ -> b)



data SizedT m (i :: Nat)  a where
  Op :: Proxy i -> m a -> SizedT m i a
  NoOp :: m a -> SizedT m 0 a

wrapWithSize :: m a -> SizedT m 0 a
wrapWithSize = NoOp

wrapWithCost :: (0 <= i) => Proxy i -> m a -> SizedT m i a
wrapWithCost = Op

isAtMost :: (n <= i) => Proxy i -> SizedT m n a -> SizedT m i a
isAtMost x (Op _ a) = Op x a
isAtMost x (NoOp a) = Op x a

runSizedT :: SizedT m i a -> m a
runSizedT (Op _ m) = m
runSizedT (NoOp m) = m


instance Functor f => SizedFunctor (SizedT f) where
  sfmap f (Op x a) = Op x (fmap f a)
  sfmap f (NoOp a) = NoOp (fmap f a)

instance Applicative f => SizedApplicative (SizedT f) where
  spure = NoOp . pure
  -- (NoOp a) |*> (NoOp b) = NoOp (a *> b)
  -- (Op x a) |*> (NoOp b) = Op x (a *> b)
  -- (NoOp a) |*> (Op y b) = NoOp (a *> b)
  -- (Op (x :: Proxy i) a) |*> (Op (y :: Proxy j) b) = Op x (a *> b)

  (NoOp a) |<*> (NoOp b) = NoOp (a <*> b)
  (NoOp a) |<*> (Op y b) = Op y (a <*> b)
  (Op x a) |<*> (NoOp b) = Op x (a <*> b)
  (Op (x :: Proxy i) a) |<*> (Op (y :: Proxy j) b) = Op (Proxy :: Proxy (Max i j)) (a <*> b)


instance Monad m => SizedMonad (SizedT m) where
  (Op (Proxy :: Proxy i) a) |>>= (m :: a -> SizedT m j b) = Op (Proxy :: Proxy (i + j)) (a >>= (\k -> runSizedT $ m k))
  (NoOp a) |>>= (m :: a -> SizedT m j b) = Op (Proxy :: Proxy i) (a >>= (\k -> runSizedT $ m k))



-- All SizedT are functors for KnownNats
instance  (KnownNat t, Functor f) => Functor (SizedT f t)  where
  fmap = sfmap

-- 0 has instances for all of these, since  Max 0 0 = 0 and (0+0) = 0
instance Applicative f => Applicative (SizedT f 0)  where
  pure = pure
  (<*>) = (<*>)

instance Monad m => Monad (SizedT m 0) where
    return = sreturn
    (>>=) = (|>>=)


type SizedIO = SizedT IO