gistfile1.txt

module Free

%access public export

data Free : (Type -> Type) -> Type -> Type where
  MkFree : f (Free f a) -> Free f a
  Pure : a -> Free f a
  
implementation Functor f => Functor (Free f) where
  map f = go where
    go (Pure a) = Pure (f a)
    go (MkFree fa) = MkFree (go <$> fa)

implementation Functor f => Applicative (Free f) where
  pure = Pure
  (Pure a) <*> (Pure b) = Pure $ a b
  (Pure a) <*> (MkFree mb) = MkFree $ map a <$> mb
  (MkFree ma) <*> b = MkFree $ (<*> b) <$> ma

implementation Functor f => Monad (Free f) where
  (MkFree x) >>= f = MkFree (map (>>= f) x)
  (Pure r) >>= f = f r

liftF : (Functor f) => f r -> Free f r
liftF x = MkFree (map Pure x)

gistfile2.txt

Free.idr:10:3:
Prelude.Functor.Free.Free f implementation of Prelude.Functor.Functor, method map is possibly not total due to: Prelude.Functor.Free.Free f implementation of Prelude.Functor.Functor, method map, go
Free.idr:16:3:
Prelude.Applicative.Free.Free f implementation of Prelude.Applicative.Applicative, method <*> is possibly not total due to: Free.MkFree
Free.idr:21:3:
Prelude.Monad.Free.Free f implementation of Prelude.Monad.Monad, method >>= is possibly not total due to: Free.MkFree
./Prelude/Monad.idr:24:5:
Prelude.Monad.Free.Free f implementation of Prelude.Monad.Monad, method join is possibly not total due to: Prelude.Monad.Free.Free f implementation of Prelude.Monad.Monad, method >>=
Free.idr:10:3:Cannot compile:
  Prelude.Functor.Free.Free f implementation of Prelude.Functor.Functor, method map is possibly not total due to: Prelude.Functor.Free.Free f implementation of Prelude.Functor.Functor, method map, go