[Agda] Re: Alfa and the summer school

[Thomas Hallgren]

Hi,

Sorry I have taken so long to reply to this...

 Ana Bove wrote:

> We don't know what the status is when it comes to Alfa and whether you 
> will be willing to put some work on it so it is ready for the school.

I might have some time to work on Alfa, but I am reluctant to spend a 
lot of time on it unless you think it would make a big difference.

> ... if we can connect Alfa with the version of Agda with hidden 
> arguments and primitives then we will use Alfa in the school.

The current status is (as I wrote to Bengt a few weeks ago) that Alfa 
works with the current version of Agda, but it doesn't take advantage of 
recently added features.

However, when it comes to the new features you want for the summer 
school (hidden arguments, strings, characters and numbers), Alfa already 
has its own support for them. Would switching Alfa over to doing these 
things the Agda way make a significant difference for the summer school 
participants? It probably depends on what kind of exercises you have in 
mind...

   1. Argument hiding: Alfa's argument hiding is in some ways more
      flexible than Agda's type-based mechanism, .e.g. it can easily be
      turned on and off, in other ways more limited, e.g., hiding
      applies to all uses of a particular identifier and is not
      associated with the scope of a certain binding (but this could be
      changed). I am not sure at the moment how support Agda's argument
      hiding mechanism in a good way in Alfa. It would probably require
      some thinking and some nontrivial implementation work. I am not
      sure it would be of any significant benefit to the summer school
      participants, but if you have some good ideas or give me some
      convincing arguments, I might consider working on it.

   2. Primitive types: Alfa's support for numbers, characters and
      strings is implemented as syntactic sugar for ordinary data types,
      which has the advantage that you can define functions on these
      types within the language, using pattern matching, and you can
      prove things about them. (But the current representation of
      numbers is not very easy to work with, so it should probably be
      changed.)

      Apart from nice syntax, I guess there one other reason for
      implementing these as primitives in Agda: efficiency. I had a
      quick look today, and it was very easy to switch Alfa over to
      using Agda's literals and the little built in Prelude. (But how do
      I get access to predefined functions on the predefined types? They
      are not in the Prelude...) If your summer school exercises include
      examples that require a lot of numeric computation, I guess Agda
      support for primitives might be necessary, but otherwise, the Alfa
      solution seems to have some advantages. But perhaps the advantages
      of both approaches can be combined?

I don't know what else you have been talking about, but I think there 
might be more fundamental things that need improvement. For example, 
Alfa has an option to unfold goal types, but most of the time it has no 
effect. So, often you have to figure out what expressions in the goal 
type reduce to, without any help from the tool, before you can figure 
out how to prove the goal. I am not sure if Agda already provides the 
required functionality to improve this, but I think it might make a 
bigger difference in usability than changing the argument hiding 
mechanism, for example...

-- 
Thomas H

You get absolutely nowhere by trying to redesign the world.
  - Linus Torvalds