How to read/understand the definition of the environment in type-checking?

Question

I am trying to read the code for TinyIdris, but couldn't understand one of the first definitions about environments below (because of my lack of understanding about type-checking and/or dependent types):

public export
data Env : (tm : List Name -> Type) -> List Name -> Type where
     Nil : Env tm []
     (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)

My current understanding is that the environment is for type-checking local variables. I thought it should be a dictionary from variable Names to types. And a Name represents a variable.

I tried to guess the meaning from the types (some people claim they can), but couldn't make sense of it and it does not look like a dictionary or key-value pair of variable-types. I guess there are two questions here.

1. Without prior knowledge, how should one read such a definition and understand it, say, well enough to give an example.

My main difficulty here is with the "undefined" variables such as x (and tm, vars). They came out of now here. My best guess is that they are some kind of implicit variables. But it's difficult to understand what they are or their types are. Really, if one doesn't already know type-checking, how would one guess the meaning of these, and conclude that the Env type does represent the data structure of a local environment.

2. With prior knowledge, could someone help explain what these variables mean (x, tm, vars), and how to read this definition in English? And what is (or how to construct) an example value of this based on the type definition?

An addition question: if these "undefined" variables are indeed implicit ones, what are the benefits of writing them as implicits? I don't know about others. It made it quite difficult for me to understand.

Answer 1

For 1., the way I read such a definition is by starting with the constructors "final" type. For instance, for Nil the type is Env tm [], so this construction builds an environment for the empty list of names. More interestingly, for (::): it takes some arguments (to be looked at later), and constructs an environment *for the list (x :: vars). So x must be a name, and vars a list of names. Now you can look at the arguments, to see what is needed to build such an extended context, and see you need a binder, and an environment. From this you can build examples, for instance Nil (not very interesting) or (::) b Nil if b : Binder (tm []), whatever Binder is doing.

For 2., the way I understand this is that an environment gives some data for a list of names. If the list is empty (constructor Nil), then also the environment is empty, and we have no information. If the list is non-empty, say x :: vars, then an environment is given by a) an environment for the "other variables" var and b) a binder corresponding to x, which contains the data given in Binder (tm var). This is a bit mysterious, by I guess the idea is that tm tells us "what information" a binder must hold, and that information might depend on the rest of the variables, var.