Is there a way to use inductive variants as types?

Stream: new members

[Alok Singh]

Morally, I want to do this:

inductive Test where
| a
| b

-- doesn't work, but is what I want
def test (x: Test.a) : Test.b :=
  match x with
  | .a => .b

-- works, but slightly unsatisfying
def test (x: Test) (h: x = Test.a) : Test :=
  match x with
  | .a => .b

[nrs]

inductive TestIndexer | a | b

inductive Test : (α : TestIndexer) -> Type
| mk : (x : TestIndexer) -> Test x

[nrs]

example : Test .a -> Test .b := fun t => match t with | .(.mk .a) => .mk .b

[nrs]

.(.mk .a) is used because you are matching on an inaccessible pattern determined by the type of your function

[Mitchell Lee]

What do you want x: Test.a to mean?

[Kyle Miller]

Here's a hack with coercions, assuming the meaning is "a value as a type should be the subtype with just that value":

inductive Test where
  | a
  | b

instance : CoeSort Test Type where
  coe v := { x : Test // x = v }

instance (v : Test) : CoeDep Test v v where
  coe := ⟨v, rfl⟩

def test (x: Test.a) : Test.b :=
  match x with
  | Test.a => Test.b

[nrs]

@Mitchell Lee most likely they mean to enforce type-level values of an arbitrary finite type

[Mitchell Lee]

Why would you want to define a function that only has one possible input?

[nrs]

it is a simpler case of a function that only takes 2, 3, 4, (etc.) inputs and no more

[Mitchell Lee]

By "only one possible input" I mean that the variable x can only take one possible value.

[nrs]

in this case yes but it is instructive to understand how this works to make more general cases (it is also usually something beginners will be confused about, the fact that any finite type is type-theoretically "the same" (through the equivalence to the canonical finite type of that same size)), so it is instructive to see how limiting the actual implementation is

[Kyle Miller]

I don't think we should assume that Test is supposed to be an enumeration like this in the actual application. Possibly Alok wants a version that supports subtypes-per-constructor, which my hack doesn't handle.

[Mitchell Lee]

In that case, I would suggest using the parameters of the constructor as the parameters of your function, rather than using a subtype

[Alok Singh]

the motivation for this was https://github.com/rust-lang/rfcs/pull/1450 and typescript's type narrowing