Re: Bug in PAKCS data inspection ¿?

From: Juan Carlos González Moreno <>
Date: Mon, 29 Oct 2007 12:03:16 +0100

Hi again,

El 29/10/2007, a las 9:14, Wolfgang Lux escribió:

> Juan Carlos González Moreno wrote:
>> Hi again,
>> I am sorry and i don't want to polemicize. But the question
>> is: Anyone knows and have use a similar data definition to:
>>>> data Seq a = a | a :< Seq a
>> in which use the the type variable name to define a new data
>> constructor ?
>> For me in this situation the expected error message must appear just
>> in the first line because i expect that
>> the interpreter must consider that "a" is a type variable introduced
>> in the left side of the definition and then
>> if it appears with no constructor associated in the right side then
>> this definition must be considered as a wrong
>> definition. If not the a renaming is done by the interpreter and it
>> is not clear for me how works this renaming
>> 1) data Seq a = b | b :< Seq b
>> 2) data Seq a = b | a :< Seq a
>> 3) data Seq a = b | b :< Seq a
>> 4) data Seq a = b | a :< Seq b ...
> As I wrote in my previous mail, type and value identifiers live in
> different name spaces, i.e., you can use the same name as value and
> a type identifier (and this is a reasonable choice).

I am agree also with this, but my question is why in the data
definition given
the interpreter assumes that a is a new data constructor. My students
don't understand it
and as i previous said to me it is more reasonable to understand that
this "a" is the name of
the declared type variable. But if there is several examples that
show me that is better to
understand that the "a" is a new constructor, please send me to study

> So in the four
> declarations above, the first b is considered a value identifier
> (because it is a legal data constructor declaration, as in your
> original example), but the other occurrences of b in the declarations
> can be considered only as type variables, and therefore all of the
> declarations above are rejected with a free type variable error for
> b in the second(!) constructor declaration.

Sorry, but if 1) is considered valid then i don't understand nothing
about how it is
implemented the type system declaration, because b is not previously
declared as data type, and
accept this line it is equivalent for me to the following (extended

>> data Seq a = b | b :< Seq b where b free

what is an existential type definition ¿?

> Regards
> Wolfgang

curry mailing list
Received on Di Okt 30 2007 - 10:44:51 CET

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:09 CEST