Zulip Chat Archive

Stream: new members

Topic: List of generic types


Chase Norman (Dec 29 2022 at 06:51):

I have created a type for a weighted directed graph on vertex type V:
def Graph (V: Type) := V → V → Nat
I would like to create a List, set, or other collection of Graphs with varying vertex types. However, because Graph is formally of type Type → Type, this cannot be done directly. Is there an idiomatic way to perform this kind of genericism?
Thanks.

Patrick Johnson (Dec 29 2022 at 08:49):

You can use docs4#Sigma:

def Graph (V : Type) : Type := V  V  Nat

def graph₁ : Graph Nat := λ _ _ => 0
def graph₂ : Graph Int := λ _ _ => 0

def myList : List (Σ V, Graph V) := [⟨_, graph₁⟩, _, graph₂⟩]

Eric Wieser (Dec 29 2022 at 17:51):

Note this only works if the types live in the same universe; if you'd used Type u instead of Type then you couldn't put a Graph Nat and a Graph (ulift.{37} Nat) in the same sigma type


Last updated: Dec 20 2023 at 11:08 UTC