Tagged/Untagged Inductives

Stream: general

[Mac]

I am curious as to why is the following is not a more common pattern in functional programming languages:

inductive FoobarCore : (tag : Lean.Name) → Type
| foo : FoobarCore `FoobarCore.foo
| bar : FoobarCore `FoobarCore.bar

abbrev Foobar := Sigma FoobarCore

namespace Foobar

abbrev foo : Foobar := Sigma.mk _ FoobarCore.foo
abbrev bar : Foobar := Sigma.mk _ FoobarCore.bar

instance : Coe (FoobarCore ``FoobarCore.foo) Foobar := ⟨fun x => Sigma.mk _ x⟩
instance : Coe (FoobarCore ``FoobarCore.bar) Foobar := ⟨fun x => Sigma.mk _ x⟩
instance : CoeDep Foobar n (FoobarCore n.1) := ⟨n.2⟩

end Foobar

(or a similar variant where tag is a Nat or Fin)

FoobarCore could be represented as a untagged union and Foobar as its tagged version while still keeping both type safe. This would also (I believe) more easily enable constructing subtypes of the union type.

[Reid Barton]

In Haskell (and I guess most other functional programming languages) types can only depend on things that aren't computationally relevant, usually other types. So FoobarCore has to be implemented as a tagged union because a function that matches on it learns about tag, which is in some sense already an argument of the function but not one that is accessible at runtime.