Allow implementation of interfaces using anonymous functions

[allancto]

Previous discussions:

Idris Mailing List: Functor instance for Vect Idris Mailing List: interface Prelude.Functor.Functor

Status: I believe this is a bug, and I would work on it, perhaps someone might give me some guidance? I feel like the error might come in Idris.Elab.Implementation.hs from checkInjectiveArgs, and a fix might be done in Language.Reflection.idr, but i don't actually know where to change the behavior (and certainly don't know whether trying will break everything).

Note: Prelude.Functor.Functor comments indeed say f must be a parametrised type, but the signature does not say this, so i don't even know where/ how the elaborator even knows it wants a parameterised type!!

  ||| Functors allow a uniform action over a parameterised type.
  interface Functor (f : Type -> Type) where
      map : (func : a -> b) -> f a -> f b

Attached file: ConstBool.idr

Proposed action (one of..):

• BUG: This is a bug, fix it
• FEATURE: This is a design decision, enforce paramterised type in the signature
• DOCUMENTATION ERROR: Fix the error message (which is even different when the parameter is lowercase or uppercase).
• REMARK: the implementation of map "should" satisfy some diagram chasing conditions, which in the case of a parameterised type is a "free theorem", but I don't think that's a sufficient reason for disallowing other forms of the parameter.

Thanks!

[ahmadsalim]

@allancto Thank you for the issue; I have tried to fix the formatting. Would it possible for you to use Gist for ConstBool.idr, since GitHub issues do not support attachments.

[allancto]

Thanks @ahmadsalim! I inserted the attachment as gist just now.

[allancto]

aggh link to ConstBool.idr was broken, should work now.

[ahmadsalim]

@allancto I unfortunately do not know a good answer to this language design question. Have you tried making a new thread on the mailing list asking specifically for this? Usually there are more people active there who might provide better feedback.

[david-christiansen]

The signature does say that f must be a parameterized type, right here:

interface Functor (f : Type -> Type) 

The Type -> Type bit says that part.

The reason for the injectivity requirement is that it's assumed by the unification engine during instance resolution. The behavior you're seeing is all by design. Let me explain the design a bit :-)

The first error comes from this:

-- BROKEN: "Overlapping implementation: Functor List already defined"
implementation Functor constBool where
  map func = idBool

This is because constBool is considered to be an implicit parameter, so it's saying:

"For any type constructor at all, which we'll call constBool here, idBool is an implementation of map." This is not the case. This interpretation is a general consequence of Idris's rules for automatic implicit arguments.

To say what you probably wanted to say there, write:

implementation Functor Main.constBool where
  map func = idBool

That causes the error to be the same as the upper-case version, again as a consequence of the automatic implicit argument rules which state that qualified names are never made implicit. One nice thing about the semantic coloring in the Emacs mode is that it makes it easier to see whether a given name refers to something else or is implicit, because one is green and the other purple.

The error that occurs when the name does refer to constBool or ConstBool is that user definitions aren't allowed for implementations. This is intentional, because unification during instance resolution assumes injectivity and arbitrary functions are not necessarily injective.

It might make sense to relax injectivity for named instances; however, Idris is presently working as designed.

[david-christiansen]

If you can think of a good way to make this more clear from the docs, that would be a good way to contribute!

[allancto]

David, thanks for this information, and I apologize for taking so long to respond. I would definitely like to contribute to the documentation as soon as I understand better myself how to describe the restrictions.

First, I'd like to understand how the restriction might be removed with named types. Also I'd like to understand more clearly what you mean by unification and injectivity. I'm guessing unification is "c" on page 15 of Brady 2013, the "type class argument is also treated as an implicit argument, to which we give the name c". Then what needs to be injective to make the unification work?

Second, I'd like to understand why my expectation of what should happen can't work. Here are the hypothetical code snippets.

• Preliminaries and sanity check

||| an ordinary usage of Functor
mapTwice : (Num a, Functor b) => b a -> b a
mapTwice = map twice where twice x = x + x

{- sanity check
> mapTwice [1]
[2] : List Int -- fine
-}

• What I think should be allowable and not

||| Broken-- naively expect the first case should work, second should not 
implementation Functor ConstBool where map = idBool 

mapTwice (True : ConstBool Int) -- should be ok? 
> True : Bool -- what it should be

mapTwice True -- clearly underspecified 
> "Not enough information to resolve the implementation, consider explicitly typing Bool" 
> "or explicitly naming the implementation of Prelude.Functor.Functor"

• What using a named implementation would look like?

||| named implementation alternative? 
implementation [cbFunctor] Functor namedConstBool where map = idBool 

mapTwice {namedConstBool} True -- ok? 
> True : Bool 

[Jake-Gillberg]

ping, any update on where this discussion went (if anywhere)?