How does Fin "know" not to go past its type bound?

How does Fin actually work?

data Nat = Z | S Nat

data Fin : (n : Nat) -> Type where
  FZ : Fin (S k) 
  FS : Fin k -> Fin (S k)

• Where does k come from?
• Why isn't FZ always the value of (n: Nat) + 1?
• How does Fin "know" not to exceed its type bound?

This mailing list talks about implicits, but I'm lost as to how and where these values come from.

Given this basic example:

t1 : Fin 3 
t1 = FZ    

What is t1's value? t1's type is Fin 3, but FZ experimentally (appears) to represent zero. Which is why we can "count" with it just like we do with Nat:

t2 : Fin 3 
t3 = FS (FS FZ)  -- this is equal to 2? 

But this confuses me given the constructor!

FZ : Fin (S k) 

If we're saying that t1 has type Fin 3, does that mean that k takes on the value of the n in the type? If that were the case, and FZ calls S on that Nat, then why isn't FZ representing 4?

This is obviously not the case.

So I'm completely and absolutely lost on how FZ acts like 0, and where k comes from, and how the compiler knows when k has become >= n just based on this data type.

I think what's confusing you is that you're thinking k is the value of the Fin n. It's not. It's just book-keeping to make sure the Fin n is always less than n.

Where does k come from?

In

  FZ : Fin (S k) 

k is an (erased) implicit argument. It's shorthand for

  FZ : {0 k : _} -> Fin (S k) 

so it's passed implicitly, but it's still an argument to FZ. In most cases, it can be unambiguously inferred from the context. The compiler will tell you if it can't.

Why isn't FZ always the value of (n: Nat) + 1?

FZ always represents zero*. This

t1 : Fin 3 
t1 = FZ

is the same as

t1 : Fin 3 
t1 = FZ {k = 2}

It's a zero that's less than three. These are also all zero

a : Fin 1
a = FZ

b : Fin 4
b = FZ

c : Fin 100
c = FZ

How does Fin "know" not to exceed its type bound?

Since FZ is always zero, and FS FZ is always one, and so on, it's impossible to express a Fin n with value greater than or equal to n. Let's try to create a Fin 2 of value two.

x : Fin 2
x = FS (FS FZ)  -- this won't compile

To see why this won't compile, fill in the implicits (note that FS also has an implicit argument called k):

x : Fin 2
x = FS {k = 1} (FS {k = 0} (FZ {k = ?!?}))

We're creating a Fin 2 so the outer-most FS must have S k = 2 so k = 1. Each successive FS we go down we reduce k by one (see the argument to FS is Fin k to produce a Fin (S k) - so one less). Eventually we reach FZ but by this point there's isn't a Nat to represent this value of k. The compiler balks with such a statement

If Data.Fin.FZ: When unifying:
    Fin (S ?k)
and:
    Fin 0
Mismatch between: S ?k and 0.

(Interactive):1:17--1:19
 1 | :let x = FS (FS FZ)
                     ^^

You can do the same for a Fin 2 of value three etc. Have a try.

Other qus

Given

t1 : Fin 3 
t1 = FZ    

What is t1's value? It's FZ, and FZ represents zero.

t2 : Fin 3 
t2 = FS (FS FZ)  -- this is equal to 2? 

Yes, it's two.

If we're saying that t1 has type Fin 3, does that mean that k takes on the value of the n in the type? If that were the case, and FZ calls S on that Nat, then why isn't FZ representing 4? S k takes on the value of n.

*this is actually a matter convention, but I'll avoid confusing things by going into that