idris-hackers/idris-free

Free Monads and useful constructions to work with them

idris-free's Issues

Bind not strictly positive

This snippet is taken from idris-free (https://github.com/idris-hackers/idris-free) which does not compile currently. This issue is about the error messages the compilation produces, not about the fact that Free does not compile:

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  Bind : f (Free f a) -> Free f a

instance Functor f => Functor (Free f) where
  map f (Pure x) = Pure (f x)
  map f (Bind x) = assert_total (Bind (map (map f) x))

The first error message one gets is :

Prelude.Functor.Control.Monad.Free.Free f implementation of Prelude.Functor.Functor, 
method map is possibly not total due to: Control.Monad.Free.Bind

Inspecting the docs of map gives the standard map function of the Functor interface which declares map to be total. This left me puzzled, because I was not able to get the totality state of this map implementation.

I then inspected the docs for Free

Data type Control.Monad.Free.Free : (f : Type -> Type) -> (a : Type) -> Type
    
    
Constructors:
    Pure : a -> Free f a
        
        
    Bind : f (Free f a) -> Free f a

(nothing unusual here) and finally Bind. The docs for Bind say:

Control.Monad.Free.Suspend : f (Free f a) -> Free f a
    
    
    The function is not strictly positive

I tried to find out what "strictly positive" means. Some Adga and Coq resources later (which I am not fluent with), there seems to be a problem that Free occurs on the left hand side of the constructor arrow. Again I am puzzled - why does

(::) : a -> List a -> List a 

work as a constructor for List then?

As a user of Idris, I would like that

• Idris reports that map is not total because Bind is not strictly positive
• Idris explains a bit better what exactly being strictly positive entitles
• as a bonus: that Idris provides error messages which link to an error message wiki page on Github, giving more detailed information about the nature of the error.

README

This repo looks like it contains code that I would like to use in another open-source project. However, the lack of a README makes this difficult! Would you mind adding one? Some useful information to include might be

1. What is the purpose of this repo?
2. How can I install the software?
3. How do I use the software?