Skip to content

idris-industry/idris-free

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

27 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Free/Freer Monads,Id monad (helper for free monad),coyonda,kan extensions

theory

http://okmij.org/ftp/Haskell/extensible/more.pdf

we can now forget not only return and bind but also the fmap operation, and still recover the state monad through FFree (State s) construction. We no longer have to bother defining the basic monad and functor operations in the first place: We now get not only the Monad instance but also the Functor and Applicative instances for free.

Marcelo Fiore has suggested in private communication that the above FFree construction is the left Kan extension. To highlight this point we show another derivation of FFree . Recall, if f :: ∗→∗ is a functor, we can convert f x to f a whenever we can map x values to a values. If g :: ∗→∗ is not a functor, such a conversion is not possible. We can “cheat” however: although we cannot truly fmap h :: x → a over g x , we can keep its two operands as a pair, and assume the mapping as if it were performed:

About

Free Monads and useful constructions to work with them

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Idris 100.0%