Why no e.g. Union and Singleton types?

Stream: lean4

[Tom]

In some languages like Scala and TypeScript, one can express more complex types using "type/set operations", e.g. x : Int | String (and also intersection and even negation). Those languages (incl. Haskell) also support the idea of "singleton types", e.g. x : 1 := 1.

Is this in some way fundamentally incompatible with Lean's type system/DTT?

I think I could "simulate" this functionality by using a type class (which would indicate the answer is "no"):

class Numeric (α : Type) where

instance : Numeric Nat where
instance : Numeric Float where
--- ... etc

def test [Numeric α] [HAdd α Nat α] (a : α) : α := a + 1

Hence I'm curious if there's another reason why it's not supported "natively" - the above just seems verbose.
It also forces the function to be "fully generic" rather than to work for a closed set of types, which, depending on your PoV, may or may not be a good thing.

With singleton types, I think I could write something like

structure NatS (n : Nat) where
  val : Nat
  proof : val = n
deriving Repr

instance : OfNat (NatS n) n where
  ofNat := { val := n, proof := rfl }

#eval (10: NatS 10) -- This is also a bit awkward

But again, that feels a bit obtuse/backward.

I would appreciate any insights!

[Daniel Weber]

There is docs#Sum for union types

[Daniel Weber]

For singleton types I don't think there's something better than {x : α // x = y}, but what do you want it for? You can use docs#Unique to claim that a type is a singleton

[Tom]

Thanks for reminding me about Sum. However, would Sum not force me to match on its constructors .inl/.inr. before I'm able to use the contained types:

def Numeric := Nat ⊕ Int ⊕ Float

def test2 [HAdd Numeric Nat Numeric] (a : Numeric) : Numeric := a + 1 -- this will not work

#eval test2 (.inr (.inr 2.0) : Numeric)

1. The type class specification of HAdd doesn't work, does it?
2. The call becomes more "involved"

[Tom]

As for singleton types, they can be useful esp in e.g. API interfaces. For example, if you have a function which can only take a specific set of values. E.g.

def shift (car : Car) (gear : 1 | 2 | 3 | 4 | 5) :=
-- or
def serialize (x: MyType) (format : "json" | "yaml") :=

I know these are contrived but hopefully it illustrates the point. These "one off types" can be expressed very easily and therefore people use them to express these invariants.

[Eric Wieser]

You could quite easily write custom notation for this which expands to

inductive Format | json | yaml
def serialize (x: MyType) (format : Format) :=

or you can use

import Mathlib.Data.Set.Basic

def serialize (x: MyType) (format : ({"json", "yaml"} : Set _)) :=

if you really want to use strings under the hood

[Tom]

For the singleton types, and in the examples I showed, I agree. And thanks for the Set example - TIL! Very interesting discovering such tidbits, I appreciate you sharing that! I still think it's a bit more typing than necessary :wink:

Having said that, I am more interested in the union type part of my question. Any thoughts on that? (And the "singleton" types were another convenient way of showing a union type)

[Tom]

And since we're taking about types, I would also be curious if structural types/row types are something that's feasible in DTT/Lean.