How to use Fin?

[Marko Grdinic]

data Vect : Nat -> Type -> Type where

   Nil  : Vect Z a

   (::) : a -> Vect k a -> Vect (S k) a

(++) : Vect n a -> Vect m a -> Vect (n + m) a

(++) Nil       ys = ys

(++) (x :: xs) ys = x :: xs ++ ys

data Fin : Nat -> Type where

   FZ : Fin (S k)

   FS : Fin k -> Fin (S k)

index : Fin n -> Vect n a -> a

index FZ     (x :: xs) = x

index (FS k) (x :: xs) = index k xs

t : Fin 2

t = ???

The above is copied straight from the tutorial. Fin is defined, but nothing is said of how to use it. I am not even sure how to construct it.

[Marko Grdinic]

data Fin : Nat -> Type where

FF : Fin 0

FZ : Fin (S k)

FS : Fin k -> Fin (S k)

t : Fin 2

t = FS(FS(FF))

Hmmm, it seems to be possible to do it like the above, though how would one then use FZ?

[jnk thss]

Fin n can be seen as the set of natural numbers smaller than n. Fin 2 contains the values FZ and FS FZ, which correspond to 0 and 1 respectively. (By contained I mean these are values of the type Fin 2).

FS (FS FZ) is not a member of Fin 2.

You can also use literals as Fin n values (e.g. 1 or 2)

- jnk

[Marko Grdinic]

t : Fin 2

t = Fin 2 // Does not work.

I should have made this the example in the first post. I am not sure why it is failing, but when I define F2 inside Fin (similar to FZ) it works.

Also I am not sure I understand how Fin n can be seen as the set of natural numbers smaller than n given the way it is defined.

If Fin 2 was defined as a class or a record type inside F# for example, then calling FZ would return Fin 3 wouldn't it?

Also, I've just realized that I've been thinking about Nat numbers as integers, but that does not affect what I wrote. In addition, defining t = FZ or t = FS FZ does work as you said, but in the REPL it is always reported as : Fin 2. Should FS FZ and FZ be different types?

[Marko Grdinic]

> Should FS FZ and FZ be different types?

I meant to write shouldn't. 

[Marko Grdinic]

Well, it occurs to me that if I wrote something like

t : String

t = String

that an error would be expected. I still can't grasp how both FS FZ and FZ are of type Fin 2.

[jnk thss]

t : Fin 2
t = Fin 2

can't work because Fin 2 is a type. You can't assign it as a value to t.

You can do

t1 : Fin 2

t1 = FZ

t2 : Fin 2

t2 = FS FZ

t3 : Fin 2

t3 = 0 -- equal to FZ

t4 : Fin 2

t4 = 1 -- equal to FS FZ

[Markus Pfeiffer]

Hi!

I think you're getting a few things mixed up here, in particular the *type*
Fin k (where k is a parameter of type Nat), and a *value* of type Fin k.

On Sun, Feb 28, 2016 at 04:28:30AM -0800, Marko Grdinic wrote:

> t : Fin 2
> t = Fin 2 // Does not work.

You can ask idris why it is faililng!

*test> :t Fin 2
Fin 2 : Type

but what you want is a value of type Fin 2. to do this, you call a
constructor, for example FZ

t : Fin 2
t = FZ

*test> :t t
FZ : Fin 2

This might be confusing, because the parameter k to the constructor FZ is inferred
by idris. In reality the type of FZ is as follows

*test> :set showimplicits
*test> :t FZ
Data.Fin.FZ : {k : Prelude.Nat.Nat} ->
Data.Fin.Fin (Prelude.Nat.S k)

So FZ can construct values of any type Fin (S k). (Bonus question: Why is it
(S k) not just k?).

The constructor FS is similar. Also try

t = FS (FS (FS FZ))


Cheers,
Markus

> --
> You received this message because you are subscribed to the Google Groups
> "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email
> to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Marko Grdinic]

> So FZ can construct values of any type Fin (S k). (Bonus question: Why is it (S k) not just k?). 

Well, if I set FZ to FZ : Fin k it would just act as an identity function, but in this case I guess it does not matter too much as there is FS to increment it. I've noticed that as expected, setting FZ to Fin k allows me to put in an extra FS inside the expression.

data Fin : Nat -> Type where

   FZ : Fin k

   FS : Fin k -> Fin (S k)

t : Fin 2

t = FS(FS(FZ)) -- This works

I think I get it now. Amazing that this works.

[jnk thss]

Note that by defining FZ : Fin k the type Fin n represents natural number less or equal n. That is 0, 1 and 2 are values of type Fin 2. (Where 0 is FZ and 1 is FS FZ and so on).

With FZ : Fin (S k) the type Fin n represents natural numbers less than n. 0 and 1 are the only values of type Fin 2. Also there are no values of type Fin 0 in this case.

- jnk