Juan Carlos González Moreno wrote:
>>> 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.
It is simply because "a" is a valid data constructor identifier and thus
the constructor declaration can be parsed, whereas there is no valid
parse if "a" were interpreted as a type variable (after a type
expression,
the compiler expects an operator identifier and another type expression
in a constructor declaration).
BTW, I must correct myself. Contrary to what I said in my previous mail,
declaration 2) above is in fact valid. But the other declarations are
not.
> 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 them.
I don't think it is more reasonable to understand "a" as a data
constructor. It is simply by matter of fact that it yields a
valid parse according to the Curry grammar.
>> 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
> declaration):
>>>
>
>>> data Seq a = b | b :< Seq b where b free
>
> what is an existential type definition ¿?
Sorry for the confusion, but I wasn't saying that declaration 1) is
valid. What I wanted to say is that the error is always reported for
the (:<) constructor and that in each of the four declarations, the
first occurrence of b is considered a data constructor.
Incidentally, it is in fact possible to define existential type
variables, though with a slightly different syntax, namely
data Seq a = b | forall b. b :< Seq b
(the declaration is using forall instead of the more natural exists
for compatibility with the various Haskell compilers that also support
this extension). Yet, the above declaration is almost useless as you
cannot do much with the arguments of the (:<) constructor, since all
you know is that the type of (:<)'s first argument and the element
type of its second argument are the same.
Regards
Wolfgang
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Okt 29 2007 - 13:04:59 CET