Developer's list of Open-Axiom ()

Gabriel Dos Reis | 19 Jan 2012 20:24

Re: [open-axiom-devel] Rep as language feature or convention

Bill Page <bill.page@...> writes:

| [Comment moved to this thread.]
| 
| On Thu, Jan 19, 2012 at 12:59 PM, Gabriel Dos Reis <gdr@...> wrote:
| > Ralf Hemmecke <ralf@...> writes:
| >
| > | On 01/19/2012 06:17 PM, Bill Page wrote:
| > | > Ok, so Aldor builds these into the language too. Why not Rep?
| > |
| > | Because that is just a convention and not necessary as a language
| > | construct. (cf. the thread from 2007 that I mentioned earlier).
| >
| > if the argument hinges on 'convention', then I am a bit disturbed: are
| > you claiming that  the builtin types Record, Union, Mapping, Category,
| > etc., are all free of conventions?
| >
| 
| I think there are very good reasons to consider at least Record, Union
| and Mapping as constructs that are essentially free of conventions -
| at least from the point of view of the intended application:
| expressing mathematical algorithms.

>From mathematics and semantics point of view, Record, Mapping, Unions
are just _conventional_ uses of dependent sigma-types and product-types.
They are no less conventional than saying that the language has a
distinguished name 'Rep' that can bound in a domain capsule.  It isn't
logically tenable to pretend the contrary.

|  We want a language that supports

(Continue reading)

headers

Bill Page | 19 Jan 2012 23:44

Re: [open-axiom-devel] Re: Rep as language feature or convention

On Thu, Jan 19, 2012 at 2:24 PM, Gabriel Dos Reis wrote:
> ...
> Bill Page writes:
> |
> | I think there are very good reasons to consider at least Record, Union
> | and Mapping as constructs that are essentially free of conventions -
> | at least from the point of view of the intended application:
> | expressing mathematical algorithms.
>
> From mathematics and semantics point of view, Record, Mapping, Unions
> are just _conventional_ uses of dependent sigma-types and product-types.
> They are no less conventional than saying that the language has a
> distinguished name 'Rep' that can bound in a domain capsule.  It isn't
> logically tenable to pretend the contrary.
>

OK. Although I am inclined to turn that around and talk about Record
as a limit, Union as a co-limit and Mapping/evaluation as
exponentiation first and then consider building a language inside this
category so that product-types and dependent types become expressions
in an internal language. I guess I am claiming that a large part of
such as language should not be viewed as just convention but rather
more or less determined by the context.

I don't think I can elaborate much more on this point of view for the
time being. I hope it suffices to say that I am not really disagreeing
with you. Some conventions are necessary in any language.

---

(Continue reading)

headers

Gabriel Dos Reis | 20 Jan 2012 01:02

Re: [open-axiom-devel] Rep as language feature or convention

Bill Page <bill.page@...> writes:

[...]

| ---
| 
| Mostly unrelated, but since this thread is specifically about language
| and there is one programming language that has attracted my attention
| several times lately, I wanted to ask if anyone has looked seriously
| at Google's new language Go:
| 
| http://golang.org/

I would not say "as seriously as C++ or Haskell", but yes I've looked at
it and I receive tons of messages from the go mailing lists daily.

My impression (this is just an impression) is that the initial
enthusiasm and support behind the language is fading so I am not sure it
would be a better investment than improving Spad...

[...]

| There are a few new ideas here that might make sense even in the
| context of Axiom.  I especially like the treatment of functions in Go.
| Go has function signatures with both named input and named output
| parameters. 

Are they really new ideas?

-- Gaby

(Continue reading)