[Agda] Future of Agda?

[Catarina Coquand]

My view on Agda is that we should define a core language that I think 
could/should be smaller
than the language of Agda today. For this core language we should have a 
type-checker
that should be written with the aim that it will be at least informally 
proven correct.
The type-checker should be a batch type-checker  with no support for 
interactivally filling
in proofs, it should not aim for nice printing of error messages etc. My 
experience is that most
of the complexity of Agda comes from conciderations of readability and 
constraint solving.

If we want to do extensions to the system we can then define how it is 
translated into the core
language (or describe how that core language needs to be changed, but 
here we should be careful).

We should then also have the interactive system for the language 
basically with the kind of functionality
that we have today and a translator for the full language to the core 
language.

One example is hidden (implicit) arguments, hidden arguments are 
replaced by metavariables which are later filled
in during typechecking. After typechecking it would be possible print 
the definitions without any
hidden arguments which could then be typechecked by the trusted 
typechecker if one wants.

Another example is the class system that I'm currently working on. The 
implementation now
completely removes classes and overloading during the translation fase 
and replaces them with signature/
records/projections, so they are not visible in the type-checker.
This is good for testing out the classes, but I can already see that it 
is not so nice for pretty printing
constraints where these projections might show up and also other 
problems related to the classes could
be better handled if one kept them during typechecking.


For the Agda that we have today I think we should rewrite it 
completeley, but not from scratch. I
used to think it is a good idea to restart from scratch, but I have 
changed my mind about that. If
one feels that the general structure is ok (which I think it is in Agda) 
then an incremental change is
better especially if it is someone that has not implemented the former 
version that does the reimplementation it
is a big risk that many new bugs are introduced.

To explicitly mark function that are recursive is fine, but I would like 
to have something also
to say that a function is not recursive, I think it is a good principle 
to have both flags but one is
default, just like the other flags in Agda.

Last thing on classes: it is an ongoing work so it's not a fixed 
suggestion for how they should
be.  For the moment it is basically the classes of Haskell  98 without 
any of the extensions that
are in GHC. It is also similar to axiomatic type classes in 
Isabelle/HOL.  I attach two files with
examples: one with classes and one with the translation. The translated 
code does not typecheck
since it in Agda for the moment assumes that all defs. are recursive, 
which I don't want here.


Regards

     Catarina



Peter G. Hancock wrote:

>>>>>>Pierre Hyvernat wrote (on Mon, 13 Dec 2004 at 15:08):
>>>>>>            
>>>>>>
>
>    >   * getting a smaller, better Agda (with a source code as simple
>    >   as we can get it)
>
>That is what I would like.  Of course it is much more difficult than
>feature-rich agda.
>
>    > My view is thus that we should have a "core Agda" as small and nice as
>    > possible. This would contain more or less what Agda contains now.  (I
>    > guess this is what Agda-light is aiming at.)
>
>I suggest that Agda which disallows *any* recursion is the basic level of
>Agda one wants.  (But not of course all.) 
>
>    > Together with that, we should try to design a good pluggin mechanism and
>    > an emacs interface (pretty much similar to what we use now) and good
>    > documentation.
>
>I entirely agree.  These are both interface issues.
>
>* between checker and front end.  This can be perhaps be looked at in
> the light of epigram, proof-general, alfa and such things.  
>
>* between someone's termination checker and the trusted core. 
>
>But I want to stress the importance of the IO interface.  I have to
>admit that although I broadly agree with Pierre that one wants to type
>both terminating and looping programs, I don't really see exactly how
>it should be expressed and made to work.  I was hoping to initiate
>some suggestions.  What are these abstract states and what role do
>they play?
>
>Plenty when you are specifying IO primitives, or writing programs that
>use them (I contend); but none at run-time.  The states have done their job
>by the time the program runs. 
>
>I don't think one should focus just on stream IO here (putchar and getchar);
>it is a very special case.  One might also try to imagine how the less exotic
>part of lazyml's IO, or Fudget's might work in Agda.  
>
>There is also the side issue of somehow coercing values to IO programs, as with
>the haskell show mechanism.  I expect that here "classes" come in. 
>I'd be really interested in what kind of class system is proposed.
>
>\begin{joke} 
>Is it going to be a playground for prolog programmers and
>people with a sick sense of humour, such as the Haskell class
>system has become?  
>\end{joke}
>
>Peter
>
>
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda
>  
>
-------------- next part --------------
data Times(A,B::Set) = Pair (a::A)(b::B)

data Unit = tt 

class  Eq (a::Set) :: Set exports
    (==) :: a -> a -> Bool

class  Ord (a::Set)  :: Set  extends (eqA::Eq a) exports
    (<)  :: a -> a -> Bool
 

instance eqUnit :: Eq Unit where
    (==) =  \h h' -> True 

instance ordUnit :: Ord Unit where
    (<) =  \h h' -> False 


instance eqTimes(a,b::Set)(eqa::Eq a)(eqb:: Eq b) :: Eq (Times a b) where
    (==) =   \h h' ->
             case h of 
                 (Pair a' b') -> case h' of 
                                    (Pair a0 b0) -> if a' == a0 then b' == b0 else False


instance ordTimes(a,b::Set)(orda::Ord a)(ordb:: Ord b) :: Ord (Times a b) where
    (<) =   \p p' -> case p of 
                       (Pair a' b') -> case p' of
                                          (Pair a0 b0) -> if a' < a0 then b' < b0 else False


h :: Unit -> Bool
h = \x -> x == x


f :: (x,y::Times Unit (Times Unit Unit)) -> Bool
f = \x y -> x < y

g (a::Set)(orda :: Ord a) :: a -> Bool
g =  \(h::a) -> h == h 


-------------- next part --------------
data Times(A,B::Set) = Pair (a::A)(b::B)

data Unit = tt 


Eq (a::Set) :: Set = sig
    (==) :: a -> a -> Bool

(==) (|a::Set)(|eqa :: Eq a) :: a -> a -> Bool
(==) = eqa.(==)

Ord (a::Set) :: Set = sig
    h :: Eq a 
    (<) :: a -> a -> Bool

(<) (|a::Set)(|orda :: Ord a) :: a -> a -> Bool
(<) = orda.(<)


eqUnit :: Eq Unit = struct
    (==) = \h h' -> True 
 
ordUnit :: Ord Unit = struct 
    h   = eqUnit
    (<) =  \h h' -> False 



eqTimes(a,b::Set)(eqa::Eq a)(eqb:: Eq b) :: Eq (Times a b) = struct
    (==) =   \h h' ->
             case h of 
                 (Pair a' b') -> case h' of 
                                    (Pair a0 b0) -> if (==) |a eqa a' a0  then 
                                                       (==) |b eqb b' b0  else False

ordTimes(a,b::Set)(orda::Ord a)(ordb:: Ord b) :: Ord (Times a b) = struct
    h   =   eqTimes a b orda.h ordb.h  
    (<) =   \p p' -> case p of 
                       (Pair a' b') -> case p' of
                                             (Pair a0 b0) -> 
                                                 if (<) |a |orda a' a0 then 
                                                    (<) |b |ordb b' b0 else False



h :: Unit -> Bool
h = \x -> (==) |Unit |eqUnit x x 


f :: (x,y::Times Unit (Times Unit Unit)) -> Bool
f = \x y -> (<) |(Times Unit (Times Unit Unit)) |(ordTimes Unit (Times Unit Unit) ordUnit (ordTimes Unit Unit ordUnit ordUnit))  x y 




g (a::Set)(orda :: Ord a) :: a -> Bool
g =  \(x::a) -> (==) |a |orda.h x x