On: Temporal Programming, a new name for an old paradi...

[mrkeen]

> Temporal programs, as I am attempting to define them, are of the form x' = f(x) - a recurrence relation.

Functions.

> x = x + 1 would not be valid, while x' = x + 1 would be.

Yep.

    void tick() {
      a@ = b + 1;
      b@ = a + 1;
    }

Void, oh no!

[a1369209993 → mrkeen]

> Void, oh no!

void is the unit type, not the uninhabited type. (I'm really not sure what Haskell was smoking when it messed that[0] up, but it's probably too late to fix now.)

0: Calling it Data.Void rather than something like Data.Noreturn or whatever.

[wnoise → a1369209993]

In C void is the unit type. I'm not sure why we should respect C's choice of nomenclature, when the obvious thing to call it is Unit, and an obvious thing to call an uninhabited type is Void. Haskell's choice is fine.

[louthy → a1369209993]

Void is the uninhabited type, Unit is the singleton type. Void != Unit

[a1369209993 → louthy]

No, as previously mentioned, `void` is the singleton type (the same type haskell calls `()`[0], and some other languages call `Unit`). Eg:

  void foo(int x) {
    printf("%i\n",x);
    return; /* <- inhabited */ }

0: Give or take some pedantry about `TYPE 'LiftedRep`.

[louthy → a1369209993]

The example you give is a statement, not an expression. There is no value returned, and the return-type is void, which can't be constructed. Only imperative languages, that can ignore the lack of a value from an expression (by simply moving on to the next statement), can deal with void returning functions. In Haskell this causes the end-of-the-program because it works solely with expressions, and an expression must have a value.

It's been a good 30 years since I've written any C, and I know its type-system is compromised at best, but I'm fairly sure you can't do something like this?

    void x = new void();

Or, using your foo example:

    void x = foo();

If you can then void is inhabited (and incorrectly named). I realise you could create void* and other elaborate means of claiming you have an inhabited void, but really can you legally construct one, not hack any underlying value to pretend to have one - there is a difference. If you can construct one and assign it to a variable, then it's inhabited.

Railing against Haskell when its implementation actually works correctly is a very strange position to take. The clue really is in the name empty-set = void, singleton-set = unit.

[aappleby → mrkeen]

Author here. My 'native' language is C++, though I'm productive in a half-dozen others. You can express the same snippet in just about anything, void or no.