Construct type from index in another type

Stream: new members

[mars0i]

I am a pretty raw beginner with Lean. (I'm less of a beginner with Idris, and have learned a small amount of Agda as well.) I want to do something that seems simple, but that's a little bit unusual at a beginning stage.

Given an indexed type, I want to construct a similar type with a different index. The following is an attempt at a simple proof of concept illustration.

The incOrganism definition below increments the index of an instance of a Niche k, creating a new instance, of Niche (1 + k). That works. However, I also want to be able to construct a Niche k' type itself, using a previous Niche k as a model to be (functionally) modified. Intuitively, it seems like I ought to be able to do this in Lean, but I can't figure out the right syntax, or maybe I just don't understand the relevant concepts for Lean.

@[match_pattern] -- added because of error message on inNiche below, but I don't understand why
inductive Niche (k : Nat) where
  | organism : Nat → Niche k
deriving Repr

-- organism-level niche incrementation: increment an organism's niche
def incOrganism {k : Nat} (o : Niche k) : Niche (1 + k) :=
  match o with
  | Niche.organism k => Niche.organism (1 + k) -- why can't I use succ btw?


-- Doesn't work.
/-- Generate a new niche from an old niche, incrementing the index. -/
def incNiche {k : Nat} (n : Type) : Type :=
  match n with
  | (Niche k) => Niche (1 + k)

I was able to do this in Idris, so I know it's possible with dependent types in some languages.

The error on the last line is "invalid patterns, k is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching .(Niche k)".

Why is k inaccessible to pattern matching? What do I need to do to make it accessible, if that's the right question to ask?

I thought that incNiche might need to reference Type 1 or Type 2 explicitly, and maybe it does, but adding in the type numbers at this stage produces additional errors that I don't understand. I might ask about that in a followup, unless it needs to be addressed first.

(I'm also curious why I had to add @[match_pattern] to get this far.)

Thanks! (I'm using neovim. Wow--incredible ide functionality. I'm sure VSCode and Emacs are at least as nice.)

[Kyle Miller]

The reason you can't use Nat.succ is that you're writing 1 + k rather than k + 1. The second is definitionally equal to Nat.succ k

[mars0i]

Oh! OK, fascinating. In Idris and Agda it's opposite--the successor corresponds to 1 +.

[Kyle Miller]

I'm not sure what incNiche is supposed to do, or rather what you want to us eit for

[Kyle Miller]

(A fundamental issue is that you can't do pattern matching on types themselves by the way.)

[mars0i]

I also didn't preface succ with Nat.. Not used to that yet.

[Kyle Miller]

You can also write k.succ, which expands to Nat.succ k since k : Nat

[Kyle Miller]

If you want a program-y reason why you can't pattern match on types, it's that they don't have a run time representation. They're erased when Lean is compiled to executable code.

[Kyle Miller]

A mathy reason is that type constructors aren't in general injective.

[mars0i]

Right. It's a weird thing I'm trying to do. You might not want to know. It's an experiment with the idea of using types to construct models that represent biological niches or organisms. There's a theoretical tradition of viewing niches as types of organisms. I'm exploring mapping the biological concept directly to a PL concept. However, there's also a concept of "niche construction", which occurs when organisms modify the environment in such a way as to create new niches. So to model that, you'd need types that can be constructed. Which dependent types seem to allow.

Oh, OK--cool re k.succ. Thanks.

[Kyle Miller]

Here, if you make your own "universe", it can be done:

structure Niche where
  k : Nat

structure Organism (k : Nat) where
  n : Nat
  deriving Repr

def Niche.type (n : Niche) : Type := Organism n.k

-- Make it automatic; turn a `Niche` into a type wherever it's used in a place expecting a type:
instance : CoeSort Niche Type := ⟨Niche.type⟩

-- organism-level niche incrementation: increment an organism's niche
def incOrganism {k : Nat} (o : Organism k) : Organism (k + 1) :=
  -- Syntax to reuse the fields for the new type:
  {o with}

-- Doesn't work.
/-- Generate a new niche from an old niche, incrementing the index. -/
def incNiche (n : Niche) : Niche  :=
  {k := n.k + 1}

def incOrganism' (n : Niche) (o : n) : incNiche n :=
  incOrganism o

[Kyle Miller]

The highlight is incOrganism', if I am getting what you're wanting to go for.

[Kyle Miller]

(structure is like a one-constructor inductive, but it gives you curly brace notation and projection notation)

[mars0i]

Wow--thank you so much @Kyle Miller. It's very kind of you to whip that up. I am going to have to take a little time to study it, both to learn about some of the concepts applied and to understand how it works. Very much appreciated.