Idris tutorial question? here and there 3.4.4

[philip andrew]

Hi there,

Can someone please baby-sit me?

In the Idris tutorial in 3.4.4, http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf

It defines here and there, so that we have the following code:

data Elem : a -> Vect n a -> Type where

  here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

  there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

testVec : Vect 4 Int

testVec = 3 :: 4 :: 5 :: 6 :: Nil

inVect : Elem 5 testVec

inVect = there (there here)

I'm trying to understand what's going on here, normally in lets say Javascript I would walk through the programs execution in my head and have an idea, but here I'm not sure what's going on.

Ok I understand the implicits, I don't understand what here and there are doing? Also if I change inVect's value to different combinations of here and there it fails.

Looking for hand-holding,

Philip

[Echo Nolan]

Hey Philip,

I'll help as best I can. The tutorial says "An instance of Elem x xs states that x is an element of xs." Another way of saying this is that a term of type Elem x xs is a proof that x is contained in xs. The two constructors correspond to the two ways something can be in a a Vect, either at the beginning or in the rest of it. The here constructor's type expresses the concept of a given element being at the beginning of a Vect:

here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

Given an x of type a and a Vect xs of as - we don't care about the length - the x is an element of the Vect made by tacking x onto the beginning of the given Vect. We trust Idris to figure out which x and xs we mean.

The simplest Elems look like this then:

inVect3 : Elem 3 [3]
inVect3 = here

If we explicate the implicits:

inVect3 = here {x = 3} {xs = Nil}

We're making a proof that 3 is within the single element Vect [3]. ([3] is syntactic sugar for 3 :: Nil.) We use here, 3 and the empty Vect to do so.

The there constructor lets us make proofs when the element we're talking about isn't at the beginning of the Vect.

there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

Translating, given two as, x and y and a Vect xs of as, and a proof that x is somewhere in xs, x is in the Vect made by tacking y onto the beginning of xs. Example:

inVect7 : Elem 7 [2,7]

inVect7 = there here

With the implicits:

inVect7 = there {x = 7} {y = 2} {xs = [7]} (here {x = 7} {xs = Nil})

The inVect example from the tutorial is what a did above, just a bit longer. Hope that helps!

Regards,
Echo Nolan

--
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.

[Chris Warburton]

philip andrew <phili...@gmail.com> writes:

> I'm trying to understand what's going on here, normally in lets say
> Javascript I would walk through the programs execution in my head and have
> an idea, but here I'm not sure what's going on.
> Ok I understand the implicits, I don't understand what here and there are
> doing? Also if I change inVect's value to different combinations of here
> and there it fails.

I'll assume you understand how "Nat" works; if not, do some reading on
"Peano arithmetic" ;)

== Nat ==

Nat has two constructors:

Z : Nat
S : Nat -> Nat

These can be combined in an infinite number of ways: "Z", "S Z",
"S (S Z)", etc.

From a static (typing) point of view, "Nat" doesn't tell us very much at
all, since it can always be trivially satisfied with "Z" ("Z" is a lot
like "()").

From a dynamic (value) point of view, the only thing a "Nat" tells us is
how many "S" constructors it has.

Hence, we can think of "Nat" as being the Natural numbers (the 'counting
numbers', where we're counting how many "S" wrappers there are around
"Z").

We can define types similar to "Nat" which are more informative, both
statically (stronger types) and dynamically (contain more data).

== Exactly n ==

We can define a strange type "Exactly n" which is like "Nat", except it
stores a "Nat" in its type too:

data Exactly : Nat -> Type where
eZ : Exactly Z
eS : Exactly n -> Exactly (S n)

Dynamically, an "Exactly n" value is exactly like a "Nat": all we can
use it for is counting. We can see this if we throw away the static
information:

plain : Exactly n -> Nat
plain eZ = Z
plain (eS n) = S (plain n)

However, we have more static information: an "Exactly n" value will have
"n" occurences of the "eS" constructor, hence it guarantees the
following:

guarantee : n -> Exactly n -> Bool
guarantee n e = plain e == n

In other words, "Exactly n" is like 'all Nats which are equal to n'.

== Fin t ==

We can change our constructors slightly to make a useful type called
"Fin n", which is a lot like "Exactly n" except for the guarantee that
it provides. It has two constructors, just like "Nat" and "Exactly n":

fZ : Fin (S n)
fS : Fin n -> Fin (S n)

Once again, we can throw away the type information to get back to "Nat":

plain : Fin n -> Nat
plain fZ = Z
plain (fS n) = S (plain n)

Hence, dynamically a "Fin n" is also just a counter like "Nat".

Statically, the guarantee we get from "Fin n" is that it has exactly "n"
possible values (try it for n=0, 1, 2, ... and see!).

The extra type information guarantees that:

fin : n -> Fin n -> Bool
fin n f = plain f < n

Hence we can think of "Fin n" as being like 'the Naturals up to n'. For
more info, see
http://stackoverflow.com/questions/18726164/how-can-finite-numbers-work-dependent-types

== NatLTE n m ==

"NatLTE n m" is like "Exactly n" but it stores *two* "Nat" arguments in
its type. Again, its constructors follow the same basic pattern as "Nat":

nEqn : NatLTE n n
nLTESm : NatLTE n m -> NatLTE n (S m)

We can throw away the type info to get:

plain : NatLTE n m -> Nat
plain nEqn = Z
plain (nLTESm n) = S (plain n)

Notice that again, dynamically we're just left with a counter. However,
we have some static guarantees about the value of that counter.

Notice that the two "Nat" values in our type must start out the same,
although unlike "eZ" they can start at any value. Just like "eS" and
"fS", we add an "S" with the "nLTESm" wrapper, although we also have
another "Nat" which gets passed along unchanged.

The guarantee for "NatLTE n m" is:

guarantee : n -> m -> NatLTE n m -> Bool
guarantee n m x = n + (plain x) == m

Hence we can think of "NatLTE n m" as being 'Nats which, when added to
n, produce m' or 'proof that n is less than or equal to m'.

== Elem x xs ==

"Elem x xs" is like "NatLTE n m" except its type can contain more than
just "Nat" values. Again, its constructors follow the same basic pattern
as "Nat":

Here : Elem x (x::xs)
There : Elem x xs -> Elem x (y::xs)

We can throw away the type information to get a "Nat":

plain : Elem x xs -> Nat
plain Here = Z
plain (There n) = S (plain n)

Again, dynamically a value of "Elem x xs" is only useful as a
counter. The static guarantee we get is the following:

guarantee : x -> xs -> Elem x xs -> Bool
guarantee x xs e = index' (plain e) xs == Just x

It does this by using "Here : Elem x xs" to tells us that "x" is the
head of "xs", whilst "There" tells us that "x" appears somewhere in the
tail of "xs".

Hence we can think of "Elem x xs" as being 'proof that x is somewhere in
xs'.

The reason you get compile errors when you change the "Here" and "There"
is because you're changing this proof. Since the proof tells Idris what
the index of the element is, if you change that index then the proof
will no longer work and the compiler rejects it.

== List t ==

Note that "List t" also follows the same constructor pattern as "Nat":

Nil : List t
Cons x : List t -> List t

The argument to "Cons" (the "x") adds *dynamic* data to the basic
"count the constructors" information found in "Nat". Note that we gain
no static information, regardless of what "t" is, since we might always
be given a "Nil".

We can throw away the dynamic information to get a Nat:

plain : List t -> Nat
plain Nil = Z
plain (Cons _ xs) = S (plain xs)

In the same way that we went from "Nat" to "Fin n", you might try making
a new type "FinList n t" for 'all lists of t up to length n'.

In the same way that we went from "Fin n" to "NatLTE n m", you might try
making a new type "SuffixList l1 l2" for 'proofs that l1 is a suffix of
l2'.

== Vect n t ==

"Vect n t" itself is a bit like "FinList n t", except instead of
containing all lists up to length "n", it contains *only* lists of
length "n". It follows the same constructor pattern as "Nat" and
"List t":

Nil : Vect Z t
Cons x : Vect n t -> Vect (S n) t

Notice that the "Nat" in the type of "Nil" is forced to be "Z", instead
of being "S n" for all "n" like in "Fin" (hint, that's the difference
between "Vect" and "FinList" ;) )

If we throw away the static information of "Vect n t" we get a "List t":

plain : Vect n t -> List t
plain Nil = Nil
plain (Cons x xs) = Cons x (plain xs)

If we throw away the dynamic information, we get an "Exactly n":

plain : Vector n t -> Exactly n
plain Nil = eZ
plain (Cons _ xs) = eS (plain xs)

== Conclusion ==

We can add dynamic information (values) to a type by adding arguments to
the constructors; this takes us, for example, from "Nat" to "List t".

We can also add static information to a type by adding arguments to the
*type* ("strengthening" it), and use the constructors to guarantee some
invariant between all these values.

The simple pattern of two constructors: one which gives a "Foo" and
another which turns a "Foo" into a "Foo", is very powerful, and can
represent all kinds of 'linear' things, including counting, lists,
bounds, linear relationships, lengths, indexes, etc.

Regards,
Chris

PS: This has gotten pretty long, I might turn it into a blog post ;)

[philip andrew]

Hi Chris and Echo,

Thanks very much for the answers. For the time being I'm going to focus on learning Purescript, then come back to this when I've mastered most of the concepts in the Purescript book.

Philip