Type* vs Type

Stream: new members

[Ching-Tsun Chou]

For "ordinary mathematics", is there any reason to use Type* rather than just Type?

The reason I ask this question is this: In my automata theory project, I had made an automaton's alphabet type and state type to be Type*. This works fine in almost all situations. But sometimes I get obscure type universe errors which I don't really understand. My intuition is that automata are very concrete mathematical objects and Type is surely "big enough" to accommodate any alphabet and state types one will ever use. So the generality of Type* is unnecessary. Is my understanding correct?

[Eric Wieser]

I assume you mean Type not TYPE?

[Notification Bot]

This topic was moved here from #new members > TYPE* vs TYPE by Ching-Tsun Chou.

[Ching-Tsun Chou]

Sorry for the typos! I've fixed them.

[Aaron Liu]

you can't (provably) fit the ordinals into Type

[Ching-Tsun Chou]

I don't need ordinals. The only "ordinals" I need to deal with are natural numbers.

[Eric Wieser]

But sometimes I get obscure type universe errors which I don't really understand

If your goal is to just make these go away, you might find that replacing Type* with Type _ in the cases where this occurs helps.

[Eric Wieser]

But I think it would be clearer with an example

[Eric Wieser]

Ching-Tsun Chou said:

Type is surely "big enough" to accommodate any [...] state types one will ever use.

if you implement a virtual function table pattern (what C++ does with vtables) using typeclasses, you can easily end up in Type 1

[Ching-Tsun Chou]

The following is an example. The definition of RegLang triggers a universe error. Currently I deal with this problem by making both A and M.State to be Type, as in the definition of RegLang'. Definitions like RegLang are located toward the top of the dependency hierarchy of my theory., so there are many other definitions and theorems in which the alphabet and states are still Type*.

import Mathlib

open Function Set Filter

class Automaton (A : Type*) where
  State : Type*
  init : Set State
  next : State → A → Set State

variable {A : Type*}

/-- A finite run of an automaton.
-/
def Automaton.FinRun (M : Automaton A) (n : ℕ) (as : ℕ → A) (ss : ℕ → M.State) :=
  ss 0 ∈ M.init ∧ ∀ k < n, ss (k + 1) ∈ M.next (ss k) (as k)

/-- The acceptance condition for finite runs.
-/
def Automaton.FinAccept (M : Automaton A) (acc : Set M.State) (n : ℕ) (as : ℕ → A) :=
  ∃ ss : ℕ → M.State, M.FinRun n as ss ∧ ss n ∈ acc

/-- The language accepted by an automaton.
-/
def Automaton.AcceptedLang (M : Automaton A) (acc : Set M.State) : Set (List A) :=
  { al | ∃ n as, M.FinAccept acc n as ∧ al = List.ofFn (fun k : Fin n ↦ as k) }

/-- A language is regular iff it is accepted by a finite-state automaton.
-/
def RegLang (L : Set (List A)) :=
  ∃ M : Automaton A, ∃ acc : Set M.State, Finite M.State ∧ L = M.AcceptedLang acc

variable {A' : Type}

def RegLang' (L : Set (List A')) :=
  ∃ M : Automaton.{0,0} A', ∃ acc : Set M.State, Finite M.State ∧ L = M.AcceptedLang acc

[Aaron Liu]

why are you bundling the state

[Aaron Liu]

ok so what category theory does to solve this issue is it makes the universes explicit

[Aaron Liu]

docs#CategoryTheory.Category

The typeclass Category C describes morphisms associated to objects of type C. The universe levels of the objects and morphisms are unconstrained, and will often need to be specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.)

[Ching-Tsun Chou]

We discussed this before. I want to define various constructions on automata (such as products and sums) and it is convenient for the state to be bundled.

[Aaron Liu]

so what you're doing here is similar I think

[Aaron Liu]

you have an alphabet instead of objects and you have a type of states instead of morphisms but it's the same thing with the universes

[Ching-Tsun Chou]

The category theory solution seems a gross overkill for my purpose. In many parts of automata theory we need to assume that the state space is finite. (The definition of a regular language is one such example.). Surely Type is big enough for us to discuss any finite sets?

[Aaron Liu]

Type is indeed good enough for finite things

[Aaron Liu]

I was a bit surprised when I saw that docs#FintypeCat is universe polymorphic

[Aaron Liu]

docs#FintypeCat.Skeleton is also universe polymorphic

[Aaron Liu]

when you're stating stuff like RegLang you should probably specialize the universe inside the definition

[Aaron Liu]

but the characterizing theorem should be universe polymorphic

[Aaron Liu]

and you should still take in {A : Type*} in the definition

[Ching-Tsun Chou]

What universe the alphabet belongs to is immaterial. If an automaton has only finitely many states, it can "distinguish" between only a finite number of subsets of the alphabet anyway.

[Aaron Liu]

that may be true, but it's so much work to prove

[Aaron Liu]

I had to prove something similar recently and it was like 200 lines

[Aaron Liu]

this was because docs#QPF.Cofix.corec was not sufficiently universe polymorphic for my needs

[Aaron Liu]

in contrast, it is trivial to pass from a universe-polymorphic version to a monomorphic version

[Ching-Tsun Chou]

Why do I want to deal with universes when I know I don't need them?

[Aaron Liu]

maybe you actually won't need them

[Aaron Liu]

but maybe you will need them, and maybe it will be convenient to have them, and maybe someone else using your work will need them