Potential issue with two types using the same primitives

[FourierTransformer]

I'm trying to use Teal to have the concept of units, and while I can create my own new types based off of a number, however I'm allowed to still add those two different types together.

Here's an example:

local type Temperature = number
local type Day = number

local temp: Temperature = 45
local birthday: Day = 34

print(temp + birthday) -- doesn't report as an error or warning

I'm not exactly sure if this is a bug, but I feel like you should only be able to get away with this if you use as to have it be treated as a different type.

[FourierTransformer]

Ah, I see how this conflicts with what is does, and overall could cause a small can of worms.

local result:Day = temp + birthday
print(result is Temperature) -- which ends up being true since type(result) == "number"

[hishamhm]

@FourierTransformer yeah, this use case is not currently covered by the type system.

The underlying concept you're looking for is whether the type system is nominal or structural. In a nominal type system, types with different names are different types. In a structural type system, types with the same data shape are the same type.

Teal's type system, as those from most programming languages, is a mix of both. For instance, record types are nominal, but function types and other primitive data types are structural.

There are languages that make a distinction between "new type declarations" and "type alias declarations", where the former declares a new distinct incompatible type and the latter declares a new name for the same type. (Haskell is especially confusing in this regard because type means a type alias, data means a new type, and newtype is a special-case new type which is erased at runtime so behaves more like an alias).

So, to keep things simple for the common cases, type in Teal means a new type for nominal types such as records, and a type alias for structural types:

So defining a type as a shorthand alias for a function works as expected:

local type F = function(number): string

local function uses_f(fn: F)
   print(fn(10) .. "!")
end

local my_f = function(n: number): string
   return "hell" .. ("o"):rep(n)
end

-- my_f was not declared as an F, but it's of the correct shape
uses_f(my_f) -- prints "helloooooooooo!"

Functions being structurally checked, this also works:

local type F = function(number): string

local function uses_f(fn: F)
   print(fn(10) .. "!")
end

local type G = function(number): string

local my_g = function(n: number): string
   return "hell" .. ("o"):rep(n)
end

-- my_g is a G, not an F, but they're the same shape
uses_f(my_g) -- prints "helloooooooooo!"

On the other hand, records are nominal, so this is not allowed:

local type Car = record
   color: string
   speed: number
end

local type Bike = record
   color: string
   speed: number
end

local function use_bike_lane(b: Bike)
   print("I'm a " .. b.color .. " bike at " .. b.speed .. "km/h!")
end

local prius: Car = {
   color = "red",
   speed = 120,
}

use_bike_lane(prius) -- ERROR: argument 1: Car is not a Bike

Currently, only record types are nominally compared; all others are structural, which makes the type declaration for them effectively behave like a type alias.

In particular, you want union types to be structural because the point of having a type U = A | B is to use U with values of type A and B, so they better be compatible.

Your report did make me spot a bug in the nominal handling of metamethods for records (look at the test case in this just-merged PR: #710).

Having said all that, it does not mean that we couldn't make the type system more nominal. For one, the example above where F and G are compatible does not sit super well with me; structurally checking named and anonymous function types is fine, but two named things perhaps should be compared by name. Your use case is also interesting, as the current behavior of local type N = number becoming a mere alias to number doesn't sound very useful.

However, making nominal numbers incompatible with each other might not be what you want either, because properly supporting units is complicated than that: making Temperature + Date being illegal is one thing, but you might still want Distance / Time to be allowed. I have no plans to add a units system as most often these can be simulated in Lua with record types (and in Teal, of course, with proper type checking!), but if there was significant demand for more complex type relations between numeric types, it wouldn't be out of the realm of possibility.

I'll do some more experiments and play a bit with the ergonomics of structural vs nominal types. All feedback in this regard is welcome!

[bjornbm]

(Warning: code examples not tested)

I'll chime in. FYI my background is in Haskell and I wrote the https://github.com/bjornbm/dimensional library which provides statically checked units (at least the SI system) as a library (as opposed to as part of the language as in F#).

Anyway, I like what I am seeing here in terms of playing with nominal typing for non-record types. That being said, I haven't played with #711 so there may be ergonomic gotchas I'm blind to.

the current behavior of local type N = number becoming a mere alias to number doesn't sound very useful.

To me this is useful only as documentation, like Haskell's type. For example, saying that we expect (but do not check/enforce) that this number argument is an angle. Not useless, but not adding any type checks beyond what number would do:

local type angle = number

local function my_sin(x: angle): number 
    return math.sin(x)
end

In the past when needing nominal typing, I have stuck my number (for example) in a record with a single element, which is a lot like a Haskell newtype except without the erasure at compile time.

local type angle = record
    value: number  -- generic pattern, could be named 'radians' here
end

local function my_sin(x: angle): number 
    return math.sin(x.value)
end

In particular, you want union types to be structural because the point of having a type U = A | B is to use U with values of type A and B, so they better be compatible.

I'm not sure about this. In Haskell the two members of a union type (e.g., Either) do not need to have the same structure. But the only thing you can really do with Either is to pattern match on Left or Right and from there on you are constrained to the appropriate structure. Not sure if my language makes sense; here is an example:

type A = String
type B = Double
type U = Either A B  -- U = A | B

fa :: a -> Bool
fa a = length a > 0

fb :: b -> Bool
fb b = b > 0

f :: U -> Bool
f u = case u of
    Left a -> fa a
    Right b -> fb b

On the topic of supporting units: I don't think this is near at hand for teal even with nominal types. I would think this would require facilities to compute/derive types (without spelling out all combinations as in @hishamhm's example, although this may be workable if you have a limited problem domain).

[hishamhm]

@bjornbm Thank you for your input, much appreciated!

In particular, you want union types to be structural because the point of having a type U = A | B is to use U with values of type A and B, so they better be compatible.

I'm not sure about this. In Haskell the two members of a union type (e.g., Either) do not need to have the same structure.

Ah, I expressed myself badly: I meant that U and A should be compatible (at least in one direction), in spite of having different names (same for U and B, of course.) -- not A and B.

I haven't played with #711 so there may be ergonomic gotchas I'm blind to.

I really hope people give #711 a try on their codebases and they let me know what/if anything breaks, and whether the things that break are checks they would like to see. (Running it on Teal's own code and test suite did require a few small changes, which can be seen in the PR diff itself, but I think the changes I spotted so far are reasonable.)

[catwell]

@hishamhm For what it's worth I ran this PR on two years of Advent of Code and my small neural networks codebase and got 0 error.

[bjornbm]

FYI a move in a similar direction, with some discussion of the rationale: unisonweb/unison#4539