Last active
February 13, 2018 19:06
-
-
Save Tritlo/aacd2d770c3d27683dba63a6ed503a8e to your computer and use it in GitHub Desktop.
OverloadedDo exploration
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment