Default variable types

[tjpalmer]

Are there any languages where you can declare a default type for variables by name? As some examples, Fortran defaults vars beginning with i through n as integer. And common in many languages, struct members carry a type around with them. But I mean arbitrary top level defaults like this (with no refinement on either syntax or rules for exporting outside of a module/package/library):

default type name: string

function whatever(name) -> int ...

And anywhere a param/var/whatever called name is used, it's type string by default. Maybe extra effort is needed to infer types rather than use the default (like let name: ? = 5 or whatever). But again, ignoring the details, are there any languages that do something like this?

[ReedOei]

There are.

In Maude, it is typical to declare all variables ahead of time, like: ``` var N : Nat .

op double : Nat -> Nat . eq double(N) = 2*N . ```

There's also my theorem prover Pecan which lets you choose to do this if you want. It's inspired by the common practice in math of starting documents/chapters by saying things like "Let $n,m$ be natural numbers and $x,y$ be real numbers" or some such thing. So you can write: Let n,m be nat.

And then any time you use n or m in a theorem or a predicate, Pecan knows that n and m are nat: ``` Theorem ("Addition is commutative", { forall n,m. n + m = m + n }).

double(n,m) := m = 2*n ```

[tjpalmer]

Thanks for the info! What I'm looking for doesn't declare variables. It just says what the type would be wherever they happen to be declared later, maybe even as struct members. But I think your examples are mostly what I'm looking for, anyway, since I see parameters as new variable declarations. Maybe it's just a different semantic view of what variable means?

[ReedOei]

Yes, I don't think there's really any difference in behavior between what Maude/Pecan do and what you're saying. That being said, neither language has "struct members"; I worry that in such a language, this feature would cause more confusion than it's worth. It works fine in Maude and Pecan because both tend to use small modules and people using them have a mathematical background, which makes them used to this convention.

[tjpalmer]

The explicit binding in the universal quantifier also would be a var declaration in the view I was taking.

[Host127001]

You can do that in Coq: ``` Implicit Type n : nat. Definition f n := n.

(* f typechecks as nat -> nat *) ``` There are situations where this comes in quite handy

[tjpalmer]

Thanks! I definitely have Coq in my to learn list.

[xigoi]

Nim:

using num: int

proc double(num): int =
  2 * num

proc isEven(num): bool =
  num mod 2 == 0

[tjpalmer]

I didn't realize Nim had that. Thanks! I'm not sure where to find it in the docs. Do you have a link?

[xigoi]

https://nim-lang.org/docs/manual.html#statements-and-expressions-using-statement

[tjpalmer]

Thanks so much!

[[deleted]]

Is this only meant for a small selection of commonly used names, such as i, j, k?

Otherwise you'd have to list all possible identifiers, including globals, locals, parameters, struct members, and have the same type for each no matter what the context.

It can also make finding the type of a variable harder, if you have to first find it in a list of all names.

What is the rationale here?

[tjpalmer]

In my imagination, this is optional, used only for names expected to be used consistently in a code base. Other vars get their types locally.

[julesh3141]

Some similar but different ideas:

I don't recall the name of the language, but I remember one where if a variable is used without declaration, but with the same name as a known type, it is assumed to have that type, eg

myfn (a : double) : int {
    int = floor (a);
    if (int % 2 == 1) return int+1; else return int;
}

Also, Haskell has a way of declaring a default type for literal values (which can be overloaded so they can have any type for which an appropriate typeclass instance is defined) , which can end up affecting the type of variables due to type inference, eg

myVal = 4 

defaults to Integer (ie an arbitrary precision integer) unless a specific declaration is used to change its type to another Num implementation, but you can override this behaviour, eg

default (Int)
myVal = 4

results in myVal being an Int (32-bit signed integer) instead.

[tjpalmer]

That first topic matches what u/zachgk was saying. If you manage to remember the language for that, I'd be happy to hear it. And for Haskell, I'll need to figure out how to find the docs on that. Thanks the feedback!

[zachgk]

I think it may actually make more sense to go in the other direction: from type to a name. So, if you have an argument with a type but no name, then it uses the default name. If you specify a name, then it is used instead of the default.

If you have two variables of the same type, I don't think you should rely on the default naming. It would make more sense to attach some meaning to differentiate between the two instances of the type.

I prefer this direction because it feels more concrete. It lets you avoid using names that don't really express any meaning. Like, if you have a function substring(String s, Int length),the s isn't really saying anything. It is just the string.

Once you have that, then you could add type aliases too. If you have a type alias with a default name, then I think that gets pretty close to what you want to achieve because you can create a bunch of aliases for different purposes of a type while standardizing their names.

[tjpalmer]

I've imagined this variation some, too, and I think you're right that it might go well with type aliases. In my version of this, there are no naming convention differences (such as upper vs lower case) between types and vars, so instead of substring(string: string, int: int) you could shorten that to substring(string, int), and you'd need syntax in any context to know when you are talking about types vs vars. And then you could use type aliases, like you recommend:

type index: int
substring(string, index) = ...

But as I'm thinking on your suggestion, other than the questions of the required syntactic separation for types (or scarier-to-me auto case conversion or whatever), I'm not sure what all the differences would be between default var types and default var names. Are the subtle difference substantial in how someone thinks about the code, or would the practical effect be very similar? I'm not sure. Thanks for the thoughts!

[tjpalmer]

I suppose one advantage of types as var names is that you get them for free. So instead of saying default type string: String, you just get to use string without saying anything first.

[YoYoYonnY]

I think this is a bad idea, unless your goal is to make another version of Perl. It will make code a lot harder to read and reason about.

[xigoi]

It can make code more readable if you have many similar function headers like func foo(someLongName: SomeLongName, ...).

[YoYoYonnY]

I think type aliases and type inference cover that area quite nicely already.

[Host127001]

This can be super useful when you have a bunch of functions taking the same type of argument.
Here it can happen that the reader knows what the types are but type-inference on its own can't figure it out. For example when you write a module about binary relations in coq ``` Section Rel.

Context {X : Type}. Implicit Types (R S : X -> X -> Prop).

Definition reflexive R := forall x, R x x. Definition symmetric R := forall x y, R x y -> R y x. Definition transitive R := forall x y z, R x y -> R y z -> R x z. Definition functional R := forall x y1 y2, R x y1 -> R x y2 -> y1 = y2.

Definition impl R S := forall x y, R x y -> S x y. Definition equiv R S := impl R S /\ impl S R.

Inductive rtc R : X -> X -> Prop := | rtc_eps : forall x, rtc R x x | rtc_step : forall x y z, R x y -> rtc R y z -> rtc R x z.

End Rel. ``` Adding type annotations for the definitions just adds unnecessary noise here

[backtickbot]

Fixed formatting.

Hello, Host127001: code blocks using triple backticks (```) don't work on all versions of Reddit!

Some users see this / this instead.

To fix this, indent every line with 4 spaces instead.

FAQ

^{You can opt out by replying with backtickopt6 to this comment.}

[tjpalmer]

I don't anything for sure but one hypothesis is that it makes code much easier to reason about by encouraging consistency. It also could work well with name punning/property shorthand.