do-notation (empty) → 0.1.0.0
raw patch · 8 files changed
+415/−0 lines, 8 filesdep +basedep +do-notationdep +indexedsetup-changed
Dependencies added: base, do-notation, indexed
Files
- ChangeLog.md +3/−0
- LICENSE +30/−0
- README.md +46/−0
- Setup.hs +2/−0
- do-notation.cabal +54/−0
- src/Control/Monad/Trans/Ix.hs +82/−0
- src/Language/Haskell/DoNotation.hs +79/−0
- test/Spec.hs +119/−0
+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for do-syntax++## Unreleased changes
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Sandy Maguire (c) 2018++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Author name here nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,46 @@+# do-notation++[](https://travis-ci.org/isovector/do-notation) | [Hackage][hackage]++[hackage]: https://hackage.haskell.org/package/do-notation+++## Dedication++> I've just locked an open door. Strange, yet symbolically compelling.+>+> Manny Calavera, Grim Fandango+++## Overview++Have you ever wanted to manage siiiick invariants with indexed monads without+giving up your regular monads in the process? `do-notation` lets you do this+with a bunch of type jiggery-pokery behind the scenes.++It also provides the `Ix m` indexed monad which is a free construction over a+regular monad `m`. Cool.+++## Usage++```haskell+{-# LANGUAGE RebindableSyntax #-}++import Language.Haskell.DoNotation+import Prelude hiding (Monad (..), pure)+```+++## Limitations++The implementation doesn't play very nicely with `do`-blocks bound via `let`.+++## Thanks++Huge shout-outs to [Csongor Kiss][kcsongor] for very patiently walking me+through the incoherent instance machinery necessary to make this all work.++[kcsongor]: http://kcsongor.github.io/+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ do-notation.cabal view
@@ -0,0 +1,54 @@+-- This file has been generated from package.yaml by hpack version 0.28.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 1c6165d413f70264592696fc50a574b3b258c9311e510f6e59be27738443ed2a++name: do-notation+version: 0.1.0.0+synopsis: Generalize do-notation to work on monads and indexed monads simultaneously.+description: Please see the README on GitHub at <https://github.com/isovector/do-syntax#readme>+category: Language+homepage: https://github.com/isovector/do-notation#readme+bug-reports: https://github.com/isovector/do-notation/issues+author: Sandy Maguire+maintainer: sandy@sandymaguire.me+copyright: 2018 Sandy Maguire+license: BSD3+license-file: LICENSE+build-type: Simple+cabal-version: >= 1.10+extra-source-files:+ ChangeLog.md+ README.md++source-repository head+ type: git+ location: https://github.com/isovector/do-notation++library+ exposed-modules:+ Control.Monad.Trans.Ix+ Language.Haskell.DoNotation+ other-modules:+ Paths_do_notation+ hs-source-dirs:+ src+ build-depends:+ base >=4.7 && <5+ , indexed+ default-language: Haskell2010++test-suite do-syntax-test+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ other-modules:+ Paths_do_notation+ hs-source-dirs:+ test+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ base >=4.7 && <5+ , do-notation+ , indexed+ default-language: Haskell2010
+ src/Control/Monad/Trans/Ix.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module Control.Monad.Trans.Ix+ ( Ix (..)+ , liftIx+ , unsafeLiftIx+ ) where++import Control.Monad (MonadPlus (..))+import Control.Monad.Indexed+import Data.Coerce (coerce)+import Data.Kind (Type)+import qualified Prelude as P+import Prelude hiding (Monad (..), pure)+++------------------------------------------------------------------------------+-- | The free indexed monad generated from a monad 'm'. Users are not expected+-- to use 'Ix' directly, but to newtype over it, specializing the kinds of 'i'+-- and 'j' as necessary.+--+-- GeneralizedNewtypeDeriving can be used to get the instances of 'IxFunctor',+-- 'IxPointed', 'IxApplicative', 'IxMonad', 'IxMonadZero' and 'IxMonadPlus' for+-- free.+newtype Ix (m :: Type -> Type) i j a = Ix+ { runIx :: m a+ }+ deriving (Functor, Applicative, P.Monad)++instance Functor m => IxFunctor (Ix m) where+ imap = fmap++instance Applicative m => IxPointed (Ix m) where+ ireturn = P.pure++instance Applicative m => IxApplicative (Ix m) where+ iap+ :: forall i j k a b+ . Ix m i j (a -> b)+ -> Ix m j k a+ -> Ix m i k b+ iap = coerce $ (<*>) @m @a @b++instance P.Monad m => IxMonad (Ix m) where+ ibind+ :: forall i j k a b+ . (a -> Ix m j k b)+ -> Ix m i j a+ -> Ix m i k b+ ibind = coerce $ (=<<) @m @a @b++instance MonadPlus m => IxMonadZero (Ix m) where+ imzero+ :: forall i j a+ . Ix m i j a+ imzero = coerce $ mzero @m @a++instance MonadPlus m => IxMonadPlus (Ix m) where+ implus+ :: forall i j a+ . Ix m i j a+ -> Ix m i j a+ -> Ix m i j a+ implus = coerce $ mplus @m @a+++------------------------------------------------------------------------------+-- | Lift an 'm' action into 'Ix m', maintaining the current index.+liftIx :: m a -> Ix m i i a+liftIx = coerce++------------------------------------------------------------------------------+-- | Lift an 'm' action into 'Ix m', changing the current index. 'unsafeLiftIx'+-- is obviously unsafe due to the fact that it can arbitrarily change the+-- index.+unsafeLiftIx :: m a -> Ix m i j a+unsafeLiftIx = coerce+
+ src/Language/Haskell/DoNotation.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableInstances #-}++------------------------------------------------------------------------------+-- | This module provides new implementations for '(>>=)', '(>>)', 'pure' and+-- 'return' so that they will work simultaneously with both regular and indexed+-- monads.+--+-- Intended usage:+--+-- @@+-- {-# LANGUAGE RebindableSyntax #-}+--+-- import Language.Haskell.DoNotation+-- import Prelude hiding (Monad (..), pure)+-- @@+module Language.Haskell.DoNotation+ ( BindSyntax (..)+ , PureSyntax (..)+ , P.Monad ()+ , IxMonad ()+ ) where++import Control.Monad.Indexed+import Data.Coerce+import Data.Kind (Constraint)+import Data.Kind (Type)+import qualified Prelude as P+import Prelude hiding (Monad (..), pure)+import System.IO (IOMode (..))+++------------------------------------------------------------------------------+-- | Typeclass that provides 'pure' and 'return'.+class PureSyntax (x :: Type -> Type) where+ pure :: a -> x a+ pure = return++ return :: a -> x a+ return = pure+++instance {-# INCOHERENT #-}+ P.Monad m => PureSyntax m where+ pure = P.pure++instance (IxMonad m, j ~ i) => PureSyntax (m i j) where+ pure = ireturn+++------------------------------------------------------------------------------+-- | Typeclass that provides '(>>=)' and '(>>)'.+class BindSyntax (x :: Type -> Type)+ (y :: Type -> Type)+ (z :: Type -> Type)+ | x y -> z+ , x z -> y+ , y z -> x where+ (>>=) :: x a -> (a -> y b) -> z b++ (>>) :: x a -> y b -> z b+ a >> b = a >>= const b++instance (P.Monad m, x ~ m) => BindSyntax m x m where+ (>>=) = (P.>>=)++instance {-# INCOHERENT #-}+ ( IxMonad m+ , x ~ m i j+ , y ~ m j k+ , z ~ m i k+ ) => BindSyntax x y z where+ (>>=) = (>>>=)+
+ test/Spec.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++import Control.Monad (void, fail)+import Control.Monad.Indexed+import Control.Monad.Trans.Ix+import Data.Coerce+import Data.Kind (Type)+import GHC.TypeLits (Nat, type (+))+import Language.Haskell.DoNotation+import Prelude hiding (Monad (..), pure)+import qualified System.IO as SIO+import System.IO hiding (openFile, Handle)+++------------------------------------------------------------------------------+-- | This module just exists to make sure 'iShouldCompile' actually compiles.+main :: IO ()+main = do+ pure ()+++------------------------------------------------------------------------------+-- | Function that uses both monads and indexed monads in do blocks.+iShouldCompile :: IO ()+iShouldCompile = do+ putStrLn "hello"+ void $ runLinear $ do+ f <- openFile "not a real file" ReadMode+ closeFile f+ pure "goodbye"+ putStrLn $ do+ c <- ['a' .. 'z']+ pure c+++------------------------------------------------------------------------------+-- | 'Linear' statically tracks the files you open and makes sure you close them+-- exactly one time.+newtype Linear (s :: Type)+ (i :: LinearState)+ (j :: LinearState) a = Linear+ { unsafeRunLinear :: Ix IO i j a+ }+ deriving (IxFunctor, IxPointed, IxApplicative, IxMonad)+++------------------------------------------------------------------------------+-- | Run the underlying IO action if you've closed all the files you opened.+runLinear+ :: (forall s. Linear s ('LinearState 0 '[])+ ('LinearState n '[]) a)+ -> IO a+runLinear = coerce+++------------------------------------------------------------------------------+-- | Data kind for tracking our linear state as the index to 'Linear'.+data LinearState = LinearState+ { linearNextKey :: Nat+ , linearOpenKeys :: [Nat]+ }+++------------------------------------------------------------------------------+-- | A wrapped 'SIO.Handle' with a phantom parameter for the ST trick.+newtype Handle (s :: Type) key = Handle+ { unsafeGetHandle :: SIO.Handle+ }+++------------------------------------------------------------------------------+-- | Open a file and track that you did it in the type system.+openFile+ :: FilePath+ -> IOMode+ -> Linear s ('LinearState next open)+ ('LinearState (next + 1) (next ': open))+ (Handle s next)+openFile = coerce SIO.openFile+++------------------------------------------------------------------------------+-- | Close a file and prove it!+closeFile+ :: IsOpen key open ~ 'True+ => Handle s key+ -> Linear s ('LinearState next open)+ ('LinearState next (Close key open))+ ()+closeFile = coerce SIO.hClose+++------------------------------------------------------------------------------+-- | Type family to detect if a file handle is already opened (ie. if it exists+-- in the open set.+type family IsOpen+ (key :: k)+ (ts :: [k]) :: Bool where+ IsOpen key '[] = 'False+ IsOpen key (key ': ts) = 'True+ IsOpen key (_x ': ts) = IsOpen key ts+++------------------------------------------------------------------------------+-- | Type family to remove a file handle from the open set.+type family Close+ (key :: k)+ (ts :: [k]) :: [k] where+ Close key (key ': ts) = ts+ Close key (_x ': ts) =+ _x ': Close key ts+