A few questions about syntax

[Alex R]

I just read the tutorial, and have played around just a tiny bit with
Agda before, and I was wondering about some of the design decisions.

1) O, S, oh, and so seem like names that are likely to get in a
programmers way; I assume that type directed disambiguation will
mitigate most of that, and if prelude can be imported hiding them and
they could be renamed, that would mitigate most of the rest, but are
Zero and Succ that much more difficult to use (I can't think of better
names for oh and so)?

2) What was the motivation for sticking to the more conventional
syntax rules as opposed to Agda's mixfix parsing tricks?

3) Is there any hope for (or any reason against) a more liberal view
of identifiers (like Agda's)? I kinda like being able to name a term
that represents a proof of equality "a=b" or "a≡b"

Sorry if these have already been answered elsewhere.

[Jason Dagit]

This is of course completely unofficial and just my sense of things.
I'm sure someone more official will weigh in.

I like to think of Idris as dependently typed Haskell. Agda on the
other hand seems to be a haskell inspired experiment in dependently
typed theorem proving.

Put another way, I think idris mostly borrows haskell ideas (type
classes, syntax to a large degree); whereas Agda experiments more to
find out what is interesting (mixfix, unicode craziness, module system
that seems quite (overly?) complex). Agda programs are meant as
proofs first and runnable things second. Idris seems to flip those
priorities.

I say that without being an expert in either idris or agda, so please
take it with a grain of salt :)

Jason

[Edwin Brady]

On 28 Feb 2012, at 04:51, Alex R wrote:

> I just read the tutorial, and have played around just a tiny bit with
> Agda before, and I was wondering about some of the design decisions.
>
> 1) O, S, oh, and so seem like names that are likely to get in a
> programmers way; I assume that type directed disambiguation will
> mitigate most of that, and if prelude can be imported hiding them and
> they could be renamed, that would mitigate most of the rest, but are
> Zero and Succ that much more difficult to use (I can't think of better
> names for oh and so)?

I've always preferred O and S because they're short and Nats are common, but now that literals are overloaded, that may not be so important. Type directed disambiguation does make it less of a problem, and I'd encourage distinguishing variables and constructors by the case of the initial letter in general (although it isn't required) to help too.

I'm not against changing things if it turns out to be a bad idea...

> 2) What was the motivation for sticking to the more conventional
> syntax rules as opposed to Agda's mixfix parsing tricks?

> 3) Is there any hope for (or any reason against) a more liberal view
> of identifiers (like Agda's)? I kinda like being able to name a term
> that represents a proof of equality "a=b" or "a≡b"

To take these together - I'm not really that keen on Agda's more liberal syntax. It's probably a matter of taste, but I find names like "a=b" harder to read since it looks too much like the type "a = b". I think also syntax rules will be more flexible especially when building DSLs.

Also, perhaps more importantly, syntax just isn't something I want to experiment too much with (as Jason said) - I'd rather keep the parser easy to implement and use features I'm already familiar with, and take the time to experiment elsewhere. I don't mind if anyone else wants to have a go though!

Edwin.

[Alex Rozenshteyn]

Cool. Thanks for the reply.

--
          Alex R