Skip to content

Instantly share code, notes, and snippets.

@bigs
Last active August 18, 2020 19:33
Show Gist options
  • Save bigs/326e314f3335bcf1872773afa64a0d82 to your computer and use it in GitHub Desktop.
Save bigs/326e314f3335bcf1872773afa64a0d82 to your computer and use it in GitHub Desktop.
module Libgit.Git
import Control.Monad.Reader
||| An abstract token representing the initialized libgit2 state. Its
||| constructor is purposefully not exported, a context can only be created
||| via `runGitT`.
export
data GitContext : (i : Type) -> Type where
MkGitContext : GitContext i
public export
data GitT : (i : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
MkGitT : ReaderT (GitContext i) m a -> GitT i m a
unGitT : GitT i m a -> ReaderT (GitContext i) m a
unGitT (MkGitT x) = x
public export
implementation Functor m => Functor (GitT i m) where
map f (MkGitT x) = MkGitT (f <$> x)
public export
implementation Applicative m => Applicative (GitT i m) where
pure x = MkGitT (pure x)
MkGitT f <*> MkGitT x = MkGitT (f <*> x)
public export
implementation Monad m => Monad (GitT i m) where
MkGitT x >>= f = MkGitT $ x >>= unGitT . f
public export
implementation HasIO m => HasIO (GitT i m) where
liftIO action = MkGitT $ liftIO action
module Control.Monad.Reader
public export
record ReaderT (stateType : Type) (m: Type -> Type) (a: Type) where
constructor MkReaderT
runReaderT : stateType -> m a
public export
implementation Functor f => Functor (ReaderT stateType f) where
map f (MkReaderT g) = MkReaderT (\st => map f (g st))
public export
implementation Applicative f => Applicative (ReaderT stateType f) where
pure x = MkReaderT (\st => pure x)
(MkReaderT f) <*> (MkReaderT a) =
MkReaderT (\st =>
let f' = f st in
let a' = a st in
f' <*> a')
public export
implementation Monad m => Monad (ReaderT stateType m) where
(MkReaderT f) >>= k =
MkReaderT (\st => do v <- f st
let MkReaderT kv = k v
kv st)
public export
implementation HasIO m => HasIO (ReaderT stateType m) where
liftIO f = MkReaderT (\_ => liftIO f)
@bigs
Copy link
Author

bigs commented Aug 18, 2020

3/5: Building Libgit.Git (src/Libgit/Git.idr)
src/Libgit/Git.idr:67:35--67:41:While processing right hand side of liftIO at src/Libgit/Git.idr:67:3--69:1:
Trying to use linear name action in non-linear context at:
67        liftIO action = MkGitT $ liftIO action

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment