3
$\begingroup$

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.

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

$\endgroup$
5
  • $\begingroup$ Since the code is in Idris, what's your background knowledge in Idris? $\endgroup$
    – Trebor
    Commented Dec 9, 2023 at 17:45
  • $\begingroup$ @Trebor I know Haskell, and know the parts of Idris that are similar to Haskell. So, a beginner here. I can also follow if a dependent type function is explained in detail. $\endgroup$
    – tinlyx
    Commented Dec 10, 2023 at 0:50
  • $\begingroup$ For your added question: Does this answer the question? $\endgroup$
    – Trebor
    Commented Dec 10, 2023 at 4:42
  • $\begingroup$ The other question is: how familiar are you with indexed inductive types? This is the main source of complexity here. $\endgroup$ Commented Dec 11, 2023 at 9:17
  • $\begingroup$ @MevenLennon-Bertrand Indeed, I'm only familiar with the very basic Vec. I am familiar with non-indexed inductive types such as binary trees. For the indexed inductive type, the multiple "undefined" variables made it difficult for me to guess the meaning of the overall type. They are probably not really undefined, they just appear without types, and I couldn't recover them. $\endgroup$
    – tinlyx
    Commented Dec 11, 2023 at 9:35

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Thanks for the answer. Could you help explain where x is coming from in (::) b Nil? I think its type is Env tm [x]. But I am not sure what this value x is. Also, I am not sure what value tm should have. The type data Env : (tm : List Name -> Type) -> List Name -> Type seems to say that Env is a function from tm to tm. $\endgroup$
    – tinlyx
    Commented Dec 12, 2023 at 0:34
  • $\begingroup$ Indeed, the type of (::) b Nil is Env tm [x] for any x. My intuition is that the "structure" of an environment Env tm vars does not depend on the names of the variables in vars, only on the length of vars. Only Binder might use the name information through tm. $\endgroup$ Commented Dec 12, 2023 at 9:38
  • $\begingroup$ For your second question: reading what Binder t does, it basically stores a t with some extra information. So Env takes a data parameterized by lists of names tm : List Name -> Type, and a list of names vars, and builds what is morally a list the same length as vars, containing for each entry some binder related information, and an element of tm over the preceding prefix in the list vars. I am unsure whether thinking of Env as mapping List Name -> Type to itself is a useful intuition… $\endgroup$ Commented Dec 12, 2023 at 9:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.