Quote from AntC on November 10, 2019, 10:33 am

Quote from johnwcowan on November 10, 2019, 5:57 am

Quote from AntC on November 10, 2019, 5:20 am

 

I believe that (modulo contra/covariance, if available) overloading functions on their return type alone is a mistake.  Java does allow it, but only if the argument types are also different.

Haskell allows overloading on the return type as a matter of course. (There's nothing special about the return type vs the argument(s) type(s).) Example below.

What is more, as I've said before, there is no unique integer division operator.  There are at least six with reasonable uses, all of them obeying the basic law n = dq + r.  I would never overload / to mean any specific one of them.

It's more that if you don't treat argument types especially, you need some other mechanism to fix types. In case of Haskell's numeric methods, they insist on the same type for both arguments and the result. That's arbitrary/it's easy to imagine a different rule. In the case of the division operator / INT division is not supported out-of-the-box for /; you can of course declare your own overloading.

'Outside in' might see the denominator(z) and infer z to be RAT.

That by no means follows either.  In the Lisps, denominator is overloaded and returns 1 when applied to an integer, as is mathematically correct.  That's most useful with either dynamic types or Haskell-style ad hoc polymorphism.

The boon of Hindley-Milner type inference is that we don't need to declare the type of every temp variable or intermediate result. Nobody would want to be forced to annotate the type of subexpression (y / 7).

Absolutely.  Fortunately, without return type overloading it's not a problem.  If anyone knows of a strong use case for return type overloading, I'd like to hear it.

Haskell standard library function read takes a Char String as argument, returns that parsed into some type. Is "7" to be parsed as Int/Integer/Int32/etc, Float/Double, Complex, String, what? That's determined by the result type:

 

x INT;   x := read "7";
y Float; y := read "7";  // returns Float 7.0

Why is that useful? Suppose you're parsing CSVs or HTML/XML/JSON or indeed a Haskell source program. The grammar tells what lexeme to parse next; the lexer tries to parse one of them; if successful, returns it paired with the remainder of the input string to continue parsing; if not returns failure with the input not advanced.

More complex example (more difficult to explain to a general audience): Without return type overloading, monadic programming would be all but impossible. The expected return type is given either by the last element's return step; or even outside the monad block by the code that consumes its result. There's typically a long sequence of steps before the return. (For safety's sake, most people put a type annotation at the start of the block, but that's not essential.)

We might even omit the declarations for x, y and leave the compiler to infer they're RAT. Nevertheless it's a sanity check to declare types for 'important' variables and functions and of course for data elements residing in the database.

Exactly.

With 'full unification' it doesn't matter whether inference goes outside in or inside out or (pragmatically) both. If there's an inconsistency, it'll be found somewhere. Of course the compiler might 'blame' the wrong declaration or subexpression, just as Erwin's so-called "analyst".

My concern is that if you don't write any type declarations but you do make a type error of exactly the right kind,

How can you make a type error if you didn't put any declarations/annotations? If there's inconsistency between the inferred type of some token in different parts of the program, the program must be rejected even though (usually) absent declarations allow the compiler to make good-enough guesses.

the compiler may fail to report it because it made a completely different set of assumptions than you did.

The whole point of Erwin's anecdote is that there's no 'right' set of assumptions. The programmer's assumptions/inferences are no more valid than those the compiler makes from the source text.

Your program will not crash in that case, but it may have extremely mysterious bugs.  (This happened not to me but to a friend of mine.)

Well-type programs can't go wrong. It's perfectly possible that ill-typed programs won't go wrong either (until they meet strange data in the small hours of January 1st, of course). But we don't risk it. Your "friend" must have been using the wrong language or the wrong compiler.

 

Quote from Dave Voorhis on November 10, 2019, 10:38 am

Quote from AntC on November 10, 2019, 10:33 am

Quote from johnwcowan on November 10, 2019, 5:57 am

Your program will not crash in that case, but it may have extremely mysterious bugs.  (This happened not to me but to a friend of mine.)

Well-type programs can't go wrong. It's perfectly possible that ill-typed programs won't go wrong either (until they meet strange data in the small hours of January 1st, of course). But we don't risk it. Your "friend" must have been using the wrong language or the wrong compiler.

It highlights the fact that whilst well-typed programs can't go wrong, well-typed programmers can go wrong when their understanding of the type system doesn't match the compiler's understanding of the type system.

Quote from AntC on November 10, 2019, 10:59 am

Quote from Dave Voorhis on November 10, 2019, 9:28 am

Quote from AntC on November 10, 2019, 4:48 am

I think support for tagged unions could easily be slotted into RM Pre 4 and 5, using Selectors with zero or more components. (The zero components would provide enumerated types like TYPE DayofWeek = Monday() | Tuesday() | ... | Sunday().) But these Selectors are not multiple PossReps for the same set of values. (Hence in my invented syntax I didn't use comma separators.) Rather, the different Selector name indicates a distinct value not representable using another Selector. I suppose you might combine tagged unions/enumerations with multiple PossReps in the TTM sense:

TYPE DayofWeek = Monday(), Lundi() | Tuesday(), Mardi() | ... | Sunday(), Dimanche();

Seems reasonable. Though I'd suggest simply this:

TYPE DayofWeek = Monday, Lundi | Tuesday, Mardi | Wednesday, Mercredi | Thursday, Jeudi | Friday, Vendredi | Saturday, Samedi | Sunday, Dimanche;

(I've left out ellipses to avoid any possible confusion between syntax and meta-syntax.)

Fair enough. I'm not claiming any expertise on Tutorial D syntax.

I.e., without parentheses, because parentheses suggest selector invocations inside the type definition, which doesn't make sense.

You would use them to select a value of the given type as usual, so this would be valid:

VAR today DayofWeek;
today := Sunday();

I assume references to existing types would be allowed. E.g...

TYPE MaybeInteger = INTEGER | Nothing;

Yes allowed; but no that's not how to do it. That's not a tagged union but an untagged union in C/C++ style. We don't want them. We do want a parameterised/polymorphic type:

TYPE Maybe a = Just a | Nothing;

ALIAS MaybeInteger = Maybe Integer;   // not a distinct type, merely a shorthand supplying a parameter for an already-declared type.

...Such that this is valid:

VAR v MaybeInteger;
v := 3;
v := Nothing;

In code that examines v how do you discriminate an Integer from a Nothing? You need a tag, and probably a case statement with pattern match:

v := Just 3;

case v of { Just x -> ... x ...;  // x bound to 3 within scope of the tag

           Nothing -> ... }           // x not in scope/no value to bind it to

 

Of course, it should also be valid to re-use Nothing:

TYPE MaybeInteger = INTEGER | Nothing;
TYPE MaybeRational = RATIONAL | Nothing;

No you don't want to reuse Nothing. That would break RM Pre 1 "the sets S1 and S2 shall be disjoint;". I.e. the sets of values in distinct types. You need shorthand

ALIAS MaybeRational = Maybe Rational;

VAR w MaybeRational;

w := Just 3.0;

w := Nothing;

But assuming that's valid, in the following...

VAR v INIT(Nothing);

...what would the type of v be?

Inferred v :: Maybe a. In which a is a unknown type, waiting to be improved from inference/solving at usage sites. OK I just introduced parametric polymorphism into Tutorial D. I guess that takes it beyond tutorial level; but I would expect an industrial D to cope.

Such things would need to be spelled out.

Ideally, the language (I assume Tutorial D) would need appropriate control structures and mechanisms, such that declaring a variable or parameter of type MaybeInteger obligates the programmer to handle both INTEGER and Nothing cases wherever necessary. That's something we've discussed before and can be found in the archives.

Yes I showed Haskell's/many FP language's case statement with binding to the components of the tagged value localised within the case branches. These are all well-understood requirements with well-understood approaches. (Presumably Tutorial D has a similar facility to 'unpack' a PossRep safely, given that different PossReps might have different/ly named components? Or do you have to extract each THE_ component individually with excessive circumlocution?)

Quote from Dave Voorhis on November 10, 2019, 2:08 pm

Quote from AntC on November 10, 2019, 10:59 am

Quote from Dave Voorhis on November 10, 2019, 9:28 am

Quote from AntC on November 10, 2019, 4:48 am

I think support for tagged unions could easily be slotted into RM Pre 4 and 5, using Selectors with zero or more components. (The zero components would provide enumerated types like TYPE DayofWeek = Monday() | Tuesday() | ... | Sunday().) But these Selectors are not multiple PossReps for the same set of values. (Hence in my invented syntax I didn't use comma separators.) Rather, the different Selector name indicates a distinct value not representable using another Selector. I suppose you might combine tagged unions/enumerations with multiple PossReps in the TTM sense:

TYPE DayofWeek = Monday(), Lundi() | Tuesday(), Mardi() | ... | Sunday(), Dimanche();

Seems reasonable. Though I'd suggest simply this:

TYPE DayofWeek = Monday, Lundi | Tuesday, Mardi | Wednesday, Mercredi | Thursday, Jeudi | Friday, Vendredi | Saturday, Samedi | Sunday, Dimanche;

(I've left out ellipses to avoid any possible confusion between syntax and meta-syntax.)

Fair enough. I'm not claiming any expertise on Tutorial D syntax.

I.e., without parentheses, because parentheses suggest selector invocations inside the type definition, which doesn't make sense.

You would use them to select a value of the given type as usual, so this would be valid:

VAR today DayofWeek;
today := Sunday();

I assume references to existing types would be allowed. E.g...

TYPE MaybeInteger = INTEGER | Nothing;

Yes allowed; but no that's not how to do it. That's not a tagged union but an untagged union in C/C++ style.

No, I'm specifically suggesting that it be a tagged union, selectable on any or Nothing via something like:

VAR p MaybeInteger;
p := 3;
CASE (p);
  WHEN IS INTEGER THEN r := p + 5;
  WHEN IS Nothing THEN WRITELN("Eeek!");
END;

We don't want them. We do want a parameterised/polymorphic type:

TYPE Maybe a = Just a | Nothing;

ALIAS MaybeInteger = Maybe Integer;   // not a distinct type, merely a shorthand supplying a parameter for an already-declared type.

...Such that this is valid:

VAR v MaybeInteger;
v := 3;
v := Nothing;

In code that examines v how do you discriminate an Integer from a Nothing? You need a tag, and probably a case statement with pattern match:

v := Just 3;

case v of { Just x -> ... x ...;  // x bound to 3 within scope of the tag

           Nothing -> ... }           // x not in scope/no value to bind it to

Of course, it should also be valid to re-use Nothing:

TYPE MaybeInteger = INTEGER | Nothing;
TYPE MaybeRational = RATIONAL | Nothing;

No you don't want to reuse Nothing. That would break RM Pre 1 "the sets S1 and S2 shall be disjoint;". I.e. the sets of values in distinct types. You need shorthand

ALIAS MaybeRational = Maybe Rational;

VAR w MaybeRational;

w := Just 3.0;

w := Nothing;

But assuming that's valid, in the following...

VAR v INIT(Nothing);

...what would the type of v be?

Inferred v :: Maybe a. In which a is a unknown type, waiting to be improved from inference/solving at usage sites. OK I just introduced parametric polymorphism into Tutorial D. I guess that takes it beyond tutorial level; but I would expect an industrial D to cope.

No, I do want to reuse Nothing, but treat the NothingS as not the same Nothing. I thought we might be onto something simple and elegant, but I guess not; things are looking better back at the IM. :-)

I presume your approach is inherently necessary. Having not thought this through at all, I'm happy to accept that it is (if it is.)

Such things would need to be spelled out.

Ideally, the language (I assume Tutorial D) would need appropriate control structures and mechanisms, such that declaring a variable or parameter of type MaybeInteger obligates the programmer to handle both INTEGER and Nothing cases wherever necessary. That's something we've discussed before and can be found in the archives.

Yes I showed Haskell's/many FP language's case statement with binding to the components of the tagged value localised within the case branches.

That I don't recall, but we did come up with a syntax for Tutorial D that used a case statement to cover specific tagged values -- or a default -- probably akin to the one I used above.

These are all well-understood requirements with well-understood approaches. (Presumably Tutorial D has a similar facility to 'unpack' a PossRep safely, given that different PossReps might have different/ly named components? Or do you have to extract each THE_ component individually with excessive circumlocution?)

Extracting each THE_ component individually is how popular object-oriented programming languages do it, though 'THE_' is usually spelled '.'

Some languages provide a "using x" construct, so that rather than p := THE_a(x); q := THE_b(y) you can do something like using x {p := a; q := b}. Tutorial D doesn't have such a mechanism, but it would be easy to add. Not sure that would be in keeping with the language ethos, though.

Quote from Dave Voorhis on November 10, 2019, 2:44 pm

Quote from Erwin on November 10, 2019, 2:10 am

I once had a difference of opinion with a so-called "analyst" (who had a university degree and I didn't so by definition he was way more competent and knowledgeable than I)

What's rarely mentioned is that some university graduates got an 'A' average and some got a 'D-'. Neither is evidence of having a clue, but the latter almost certainly doesn't.

That's true of all degree and higher qualifications. Think about that next time you're in the waiting room at the dentist...

Quote from Erwin on November 10, 2019, 4:46 pm

Quote from Dave Voorhis on November 10, 2019, 2:44 pm

Quote from Erwin on November 10, 2019, 2:10 am

I once had a difference of opinion with a so-called "analyst" (who had a university degree and I didn't so by definition he was way more competent and knowledgeable than I)

What's rarely mentioned is that some university graduates got an 'A' average and some got a 'D-'. Neither is evidence of having a clue, but the latter almost certainly doesn't.

That's true of all degree and higher qualifications. Think about that next time you're in the waiting room at the dentist...

That so-called analyst got his degree just as much as the dentist did.  I'll try ***not*** to think of that when I'm there.

Quote from johnwcowan on November 10, 2019, 6:25 pm

Quote from AntC on November 10, 2019, 10:33 am

In the case of the division operator / INT division is not supported out-of-the-box for /; you can of course declare your own overloading.

You should never casually write i/j without understanding what you really want.  Truncation is the default, but almost never the Right Thing: you may want rounding, floor, ceiling, Euclidean, or balanced division depending on the use case.

Haskell standard library function read takes a Char String as argument, returns that parsed into some type. Is "7" to be parsed as Int/Integer/Int32/etc, Float/Double, Complex, String, what? That's determined by the result type:

Why is that useful? Suppose you're parsing CSVs or HTML/XML/JSON or indeed a Haskell source program. The grammar tells what lexeme to parse next; the lexer tries to parse one of them; if successful, returns it paired with the remainder of the input string to continue parsing; if not returns failure with the input not advanced.

Interesting.   However, unless there is downward information from the type assignment engine all the way to the lexer, the lexer will not know what kind of literal to get next.  I know that Haskell and Go do this ad hoc for numbers, but in the general case it seems unlikely to work right.

How can you make a type error if you didn't put any declarations/annotations? If there's inconsistency between the inferred type of some token in different parts of the program, the program must be rejected even though (usually) absent declarations allow the compiler to make good-enough guesses.

They are consistent: it's just a consistency you didn't intend.  Compilers were made to serve the programmer, not vice versa, though it sometimes seems that way.

That so-called analyst got his degree just as much as the dentist did.  I'll try ***not*** to think of that when I'm there.

The analyst presumably didn't have to pass an examination controlled by members of his own profession in order to practice, however, unlike dentist, doctors, lawyers, and actual engineers.  (I never liked being called, or calling anyone, a software engineer.)

Quote from AntC on November 10, 2019, 10:30 pm

Quote from Dave Voorhis on November 10, 2019, 2:08 pm

Quote from AntC on November 10, 2019, 10:59 am

Quote from Dave Voorhis on November 10, 2019, 9:28 am

Quote from AntC on November 10, 2019, 4:48 am

I think support for tagged unions could easily be slotted into RM Pre 4 and 5, using Selectors with zero or more components. (The zero components would provide enumerated types like TYPE DayofWeek = Monday() | Tuesday() | ... | Sunday().) But these Selectors are not multiple PossReps for the same set of values. (Hence in my invented syntax I didn't use comma separators.) Rather, the different Selector name indicates a distinct value not representable using another Selector. I suppose you might combine tagged unions/enumerations with multiple PossReps in the TTM sense:

TYPE DayofWeek = Monday(), Lundi() | Tuesday(), Mardi() | ... | Sunday(), Dimanche();

Seems reasonable. Though I'd suggest simply this:

TYPE DayofWeek = Monday, Lundi | Tuesday, Mardi | Wednesday, Mercredi | Thursday, Jeudi | Friday, Vendredi | Saturday, Samedi | Sunday, Dimanche;

(I've left out ellipses to avoid any possible confusion between syntax and meta-syntax.)

Fair enough. I'm not claiming any expertise on Tutorial D syntax.

I.e., without parentheses, because parentheses suggest selector invocations inside the type definition, which doesn't make sense.

You would use them to select a value of the given type as usual, so this would be valid:

VAR today DayofWeek;
today := Sunday();

I assume references to existing types would be allowed. E.g...

TYPE MaybeInteger = INTEGER | Nothing;

Yes allowed; but no that's not how to do it. That's not a tagged union but an untagged union in C/C++ style.

No, I'm specifically suggesting that it be a tagged union, selectable on any or Nothing via something like:

VAR p MaybeInteger;
p := 3;
CASE (p);
  WHEN IS INTEGER THEN r := p + 5;
  WHEN IS Nothing THEN WRITELN("Eeek!");
END;

No that won't work in general. A tagged union means that every value within the type carries a tag. Consider

TYPE MaritalStatus = Single | Married Date | Divorced Date | Widowed Date;

In general, there might be many tags with exactly the same typed components.

 

We don't want them. We do want a parameterised/polymorphic type:

TYPE Maybe a = Just a | Nothing;

ALIAS MaybeInteger = Maybe Integer;   // not a distinct type, merely a shorthand supplying a parameter for an already-declared type.

...Such that this is valid:

VAR v MaybeInteger;
v := 3;
v := Nothing;

In code that examines v how do you discriminate an Integer from a Nothing? You need a tag, and probably a case statement with pattern match:

v := Just 3;

case v of { Just x -> ... x ...;  // x bound to 3 within scope of the tag

           Nothing -> ... }           // x not in scope/no value to bind it to

Of course, it should also be valid to re-use Nothing:

TYPE MaybeInteger = INTEGER | Nothing;
TYPE MaybeRational = RATIONAL | Nothing;

No you don't want to reuse Nothing. That would break RM Pre 1 "the sets S1 and S2 shall be disjoint;". I.e. the sets of values in distinct types. You need shorthand

ALIAS MaybeRational = Maybe Rational;

VAR w MaybeRational;

w := Just 3.0;

w := Nothing;

But assuming that's valid, in the following...

VAR v INIT(Nothing);

...what would the type of v be?

Inferred v :: Maybe a. In which a is a unknown type, waiting to be improved from inference/solving at usage sites. OK I just introduced parametric polymorphism into Tutorial D. I guess that takes it beyond tutorial level; but I would expect an industrial D to cope.

No, I do want to reuse Nothing, but treat the NothingS as not the same Nothing. I thought we might be onto something simple and elegant, but I guess not; things are looking better back at the IM. :-)

I presume your approach is inherently necessary. Having not thought this through at all, I'm happy to accept that it is (if it is.)

Re-using Nothing won't work either. I'm not just complying with RM Pre 1: in this case TTM is aligned with well-established theory in all programming languages with tagged unions AFAIA. (To repeat: you're trying to do untagged unions, which might be a valid model, but not what I'm proposing.) Consider tags appearing in enumerations:

TYPE NumBase = Dec | Oct | Hex;

TYPE Month = Jan | Feb | ... | Oct | Nov | Dec;

IF p IS Dec THEN ...;     // what's the type of p?

As I said earlier, the appearance of the tag in the TYPE decl brings that value into existence and brings its name(s) into scope.

The tag must be unambiguous as to which type it's a value from. Why do you think " treat the NothingS as not the same Nothing" has anything simple or elegant about it? It's a recipe for confusion for both the reader and the compiler of programs.

CASE (p);
  WHEN IS Nothing THEN WRITELN("Eeek!");
  ELSE THEN r := p + 5;                                           // we still don't know the type of p, except that it's numeric

END;

Such things would need to be spelled out.

Ideally, the language (I assume Tutorial D) would need appropriate control structures and mechanisms, such that declaring a variable or parameter of type MaybeInteger obligates the programmer to handle both INTEGER and Nothing cases wherever necessary. That's something we've discussed before and can be found in the archives.

Yes I showed Haskell's/many FP language's case statement with binding to the components of the tagged value localised within the case branches.

That I don't recall, but we did come up with a syntax for Tutorial D that used a case statement to cover specific tagged values -- or a default -- probably akin to the one I used above.

These are all well-understood requirements with well-understood approaches. (Presumably Tutorial D has a similar facility to 'unpack' a PossRep safely, given that different PossReps might have different/ly named components? Or do you have to extract each THE_ component individually with excessive circumlocution?)

Extracting each THE_ component individually is how popular object-oriented programming languages do it, though 'THE_' is usually spelled '.'

Some languages provide a "using x" construct, so that rather than p := THE_a(x); q := THE_b(y) you can do something like using x {p := a; q := b}. Tutorial D doesn't have such a mechanism, but it would be easy to add. Not sure that would be in keeping with the language ethos, though.

Well yes. Probably parametric types and pattern matching are beyond Tutorial. But pattern matching is soooo simple and elegant, and delivers type safety and scoping of component names with one intuitive construct.

Quote from dandl on November 11, 2019, 12:13 am

Quote from johnwcowan on November 10, 2019, 6:25 pm

How can you make a type error if you didn't put any declarations/annotations? If there's inconsistency between the inferred type of some token in different parts of the program, the program must be rejected even though (usually) absent declarations allow the compiler to make good-enough guesses.

They are consistent: it's just a consistency you didn't intend.  Compilers were made to serve the programmer, not vice versa, though it sometimes seems that way.

I think that was the intent of PL/I. Didn't quite work out, as I recall.

That so-called analyst got his degree just as much as the dentist did.  I'll try ***not*** to think of that when I'm there.

The analyst presumably didn't have to pass an examination controlled by members of his own profession in order to practice, however, unlike dentist, doctors, lawyers, and actual engineers.  (I never liked being called, or calling anyone, a software engineer.)

Not even someone with a degree in Software Engineering from a reputable university? What would you call them?

And in my personal experience, entry to the profession is governed by the  educational establishment and government regulation, all teachers and public servants. It's advancement within the profession that is largely controlled by members of the profession.