[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Re: [Aldor-l] exports and constants

From: Ralf Hemmecke
Subject: [Axiom-developer] Re: [Aldor-l] exports and constants
Date: Mon, 24 Jul 2006 22:48:28 +0200
User-agent: Thunderbird (X11/20060516)

  Has expressions

  A ``has'' expression has the following form:

      dom has cat

  where dom is a domain-valued expression, and cat is a category-valued
  expression. A ``has'' expression may be used in any part of a program,
  but is most often used to conditionalize domains and categories. The
  result of the expression is a Boolean value which will be true if dom
  can be shown to **satisfy** the category, and false otherwise.
  The evaluation of this expression is made at run-time, ...

** my emphasis. Type satisfaction is defined in section 7.7:
  "We say that a type S satisfies the type T if any value of type S can
  be used in any context which requires a value of type T."

The compiler seems to have problems with that specification. I had a discussion about this with Antoine Hersen today.

#include "aldor"
#include "aldorio"
define CatA(s: String): Category == with;
A(s: String): CatA(s) == add;
stdout << (A("x") has CatA("x")) << newline;
stdout << (A("y") has CatA("x")) << newline;

>aldor -grun -laldor

Now let's replace
String <-- PrimitiveType
"x"    <-- String
"y"    <-- Integer

#include "aldor"
#include "aldorio"
define CatA(s: PrimitiveType): Category == with;
A(s: PrimitiveType): CatA(s) == add;
stdout << (A(String)  has CatA(String)) << newline;
stdout << (A(Integer) has CatA(String)) << newline;

>aldor -grun -laldor

I hope that someone agrees with me that this is a bit confusing.

We had a similar thing when we discussed about "Dom has Monoid(*, 1)".


reply via email to

[Prev in Thread] Current Thread [Next in Thread]