[Agda] Future of Agda?
Catarina Coquand
catarina at cs.chalmers.se
Tue Dec 14 12:19:18 CET 2004
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
More information about the Agda
mailing list