2
$\begingroup$

This is the = Type variable rule that I'm seeing through out the my course and unable to grasp it completely.

$$\dfrac{\phi \vdash \Gamma[\mathrm{ctx}] \qquad \Gamma(x) = \tau} {\phi; \Gamma \vdash x : \tau} \textsf{(ty-var)}$$

The first thing in antecedent looks like it's stating that $\Gamma$ is well-formed under the context $\phi$, is that right? What does the second thing in antecedent mean? I have a feeling of this but I am unable to get this simple rule.

$\endgroup$
  • 2
    $\begingroup$ What's $\phi$ here? $\endgroup$ – Gilles Mar 31 '16 at 10:28
  • $\begingroup$ Actually that was from ML0,pi (C) so that's called "sort type" or type of the constraint domain where type index objects are drawn. $\endgroup$ – Pushpa Mar 31 '16 at 18:01
  • $\begingroup$ i'm new to type theory and have verification(Model checking) background. So it's really new thing to me. I'm reading paper "Dependent Types in practical programming". $\endgroup$ – Pushpa Mar 31 '16 at 18:18
  • 3
    $\begingroup$ Please ask your follow-up question as a separate question. It's a completely different issue. (An interesting one, too, so I do encourage you to ask it, but please ask one question at a time.) $\endgroup$ – Gilles Mar 31 '16 at 18:43
4
$\begingroup$

Essentially, $\Gamma$ is a store that maps variables to types.

This rule says that we can deduce that a variable has a type in a context if that type is stored for our variable in the context.

The rule is deliberately simple, and is a base case for the inductive process that is type derivation.

In short, to check the type of a variable, just look it up in the environment.

$\endgroup$
  • 2
    $\begingroup$ Thanks . Any references where i could get all explanation as clear as you have stated for other rules ? $\endgroup$ – Pushpa Mar 31 '16 at 7:34
  • 3
    $\begingroup$ Maybe Types and Programming Languages by Pierce? I'm not sure, as a rule it's not exclusive to depenent types, it's in basically every type system. So I don't have a particular reference off hand, but any introduction to type theory should have it. $\endgroup$ – jmite Mar 31 '16 at 7:50
  • 2
    $\begingroup$ @Pushpa, jmite: Dependent types are in the second volume ATTAPL (both good books by the way). While the basic principle is common to most type systems, dependent types does make the formuation more complex (an introduction to type theory would just have $\dfrac{\Gamma(x)=\tau}{\Gamma \vdash x:\tau}$ because that's all you need with simple types). $\endgroup$ – Gilles Mar 31 '16 at 10:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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