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.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ What's $\phi$ here? $\endgroup$
    – Gilles 'SO- stop being evil'
    Mar 31, 2016 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, 2016 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, 2016 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 'SO- stop being evil'
    Mar 31, 2016 at 18:43

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ Thanks . Any references where i could get all explanation as clear as you have stated for other rules ? $\endgroup$
    – Pushpa
    Mar 31, 2016 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, 2016 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 'SO- stop being evil'
    Mar 31, 2016 at 10:25

Your Answer

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

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