LET REC recursive expression static typing rule











up vote
5
down vote

favorite
1












I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system.



To be more specific, we're using the textbook Essentials of Programming Languages (3e) - Friedman & Wand.






To give some rough background, here's how the author describes the typing rule for a normal let binding expression:



enter image description here



To briefly describe it for anybody unfamiliar with the notation, type-of is a function used to evaluate the type of the given expression.



According to the typing rule, we evaluate exp1 first, which would give us type $t_1$. Then we extend our current environment so $var$ is mapped to $t_1$. Using this new environment, we evaluate the $body$ of the expression which gives us our final type.



Here's a typical let binding example in the OCaml programming language:



let func (x) = x + 1 in (func 3);; (* Outputs -: int=4 *)

let func = fun (x -> x + 1) in (func 3);;
(* Equivalent but better aligned with given typing rule. *)





Here's how a let-rec recursive binding's typing rule is defined:



enter image description here



The main problem that I'm having is how to understand the order of evaluation. According to the typing rule, it seems as though we're extending the environment first with $var$ and $p$, but where are we getting the types to map them to from?










share|cite|improve this question




























    up vote
    5
    down vote

    favorite
    1












    I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system.



    To be more specific, we're using the textbook Essentials of Programming Languages (3e) - Friedman & Wand.






    To give some rough background, here's how the author describes the typing rule for a normal let binding expression:



    enter image description here



    To briefly describe it for anybody unfamiliar with the notation, type-of is a function used to evaluate the type of the given expression.



    According to the typing rule, we evaluate exp1 first, which would give us type $t_1$. Then we extend our current environment so $var$ is mapped to $t_1$. Using this new environment, we evaluate the $body$ of the expression which gives us our final type.



    Here's a typical let binding example in the OCaml programming language:



    let func (x) = x + 1 in (func 3);; (* Outputs -: int=4 *)

    let func = fun (x -> x + 1) in (func 3);;
    (* Equivalent but better aligned with given typing rule. *)





    Here's how a let-rec recursive binding's typing rule is defined:



    enter image description here



    The main problem that I'm having is how to understand the order of evaluation. According to the typing rule, it seems as though we're extending the environment first with $var$ and $p$, but where are we getting the types to map them to from?










    share|cite|improve this question


























      up vote
      5
      down vote

      favorite
      1









      up vote
      5
      down vote

      favorite
      1






      1





      I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system.



      To be more specific, we're using the textbook Essentials of Programming Languages (3e) - Friedman & Wand.






      To give some rough background, here's how the author describes the typing rule for a normal let binding expression:



      enter image description here



      To briefly describe it for anybody unfamiliar with the notation, type-of is a function used to evaluate the type of the given expression.



      According to the typing rule, we evaluate exp1 first, which would give us type $t_1$. Then we extend our current environment so $var$ is mapped to $t_1$. Using this new environment, we evaluate the $body$ of the expression which gives us our final type.



      Here's a typical let binding example in the OCaml programming language:



      let func (x) = x + 1 in (func 3);; (* Outputs -: int=4 *)

      let func = fun (x -> x + 1) in (func 3);;
      (* Equivalent but better aligned with given typing rule. *)





      Here's how a let-rec recursive binding's typing rule is defined:



      enter image description here



      The main problem that I'm having is how to understand the order of evaluation. According to the typing rule, it seems as though we're extending the environment first with $var$ and $p$, but where are we getting the types to map them to from?










      share|cite|improve this question















      I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system.



      To be more specific, we're using the textbook Essentials of Programming Languages (3e) - Friedman & Wand.






      To give some rough background, here's how the author describes the typing rule for a normal let binding expression:



      enter image description here



      To briefly describe it for anybody unfamiliar with the notation, type-of is a function used to evaluate the type of the given expression.



      According to the typing rule, we evaluate exp1 first, which would give us type $t_1$. Then we extend our current environment so $var$ is mapped to $t_1$. Using this new environment, we evaluate the $body$ of the expression which gives us our final type.



      Here's a typical let binding example in the OCaml programming language:



      let func (x) = x + 1 in (func 3);; (* Outputs -: int=4 *)

      let func = fun (x -> x + 1) in (func 3);;
      (* Equivalent but better aligned with given typing rule. *)





      Here's how a let-rec recursive binding's typing rule is defined:



      enter image description here



      The main problem that I'm having is how to understand the order of evaluation. According to the typing rule, it seems as though we're extending the environment first with $var$ and $p$, but where are we getting the types to map them to from?







      programming-languages type-theory type-checking






      share|cite|improve this question















      share|cite|improve this question













      share|cite|improve this question




      share|cite|improve this question








      edited Dec 8 at 2:11

























      asked Dec 7 at 4:51









      Seankala

      29611




      29611






















          2 Answers
          2






          active

          oldest

          votes

















          up vote
          4
          down vote



          accepted










          It seems you discovered the difference between a set of typing rules and an algorithm for type inference.



          Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. Their purpose is only to precisely define a mathematical relation $Gamma vdash t: tau$.



          Once we have such definition, we do not automatically get a type checking algorithm. That is, in general, there is no algorithm described by the rules which, given $Gamma,t,tau$, is able to test whether $Gamma vdash t: tau$ holds. (In some cases, such an algorithm could even fail to exist!)



          Similarly, we do not automatically obtain a type inference algorithm, which given $Gamma,t$ is able to find a related $tau$ (when it exists).



          The type checking/type inference algorithm must be devised independently.



          Now, it is true that in many cases the algorithms can follow the rules quite closely. The rule for non-recursive LET you mention is one nice example, since it is clear how to turn it into an algorithm. For recursive LETs, we are not that lucky.



          A typical strategy to type check/infer recursive LETs is to introduce a fresh type variable in the environment, and then perform type checking on the body while generating a set of constraints. For instance, consider this example



          let-rec f (x: int) = 1 + f(x) in f(0)


          We discover immediately that f : int -> ???. Let's introduce a fresh type variable R for the result, and say f : int -> R.



          We then type check 1 + f(x) assuming the environment f: int -> R , x: int.
          Here + is applied to arguments 1: int and f(x): R. Assuming + requires its arguments to be of the same type, this forces the constraint int = R.
          If + also returns the same type, we obtain another constraint int = R (redundant, in this case).



          Finally, we solve the constraints, discovering R = int.



          Note that in the general case we might be less lucky, since more complex types could be involved.



          let-rec f(x: int) = (2, fst(f(x-1)))


          Here, we discover f: int -> R, then we see that R must be a pair type R = A*B, then A=int (because of the 2). Moreover, we get f(x-1):R so fst(f(x-1)): A, hence B=A. We conclude f: int->(int*int).



          It is not trivial to generate these constraints, or to solve them (usually through a unification algorithm). In the scientific literature we can find several algorithms which perform this, but they are not obvious at first.






          share|cite|improve this answer






























            up vote
            4
            down vote













            Typing rules are not "code". There is no "evaluation order". All the rule is saying is: if we're given some $t_{res}$ and $t_{var}$ (and $t$ and $tenv$ and ...) such that the first two equations hold, then we can conclude the bottom equation. How you come up with the $t_{res}$ and $t_{var}$ is out of scope and not specified.



            That said, often we can read these types of rules as programs, but they are logic programs. In this context, the answer to your question is easy: you simply stick logic variables everywhere. Unification will handle the data transfer in whatever direction is needed.






            share|cite|improve this answer





















              Your Answer





              StackExchange.ifUsing("editor", function () {
              return StackExchange.using("mathjaxEditing", function () {
              StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
              StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
              });
              });
              }, "mathjax-editing");

              StackExchange.ready(function() {
              var channelOptions = {
              tags: "".split(" "),
              id: "419"
              };
              initTagRenderer("".split(" "), "".split(" "), channelOptions);

              StackExchange.using("externalEditor", function() {
              // Have to fire editor after snippets, if snippets enabled
              if (StackExchange.settings.snippets.snippetsEnabled) {
              StackExchange.using("snippets", function() {
              createEditor();
              });
              }
              else {
              createEditor();
              }
              });

              function createEditor() {
              StackExchange.prepareEditor({
              heartbeatType: 'answer',
              convertImagesToLinks: false,
              noModals: true,
              showLowRepImageUploadWarning: true,
              reputationToPostImages: null,
              bindNavPrevention: true,
              postfix: "",
              imageUploader: {
              brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
              contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
              allowUrls: true
              },
              onDemand: true,
              discardSelector: ".discard-answer"
              ,immediatelyShowMarkdownHelp:true
              });


              }
              });














              draft saved

              draft discarded


















              StackExchange.ready(
              function () {
              StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f101152%2flet-rec-recursive-expression-static-typing-rule%23new-answer', 'question_page');
              }
              );

              Post as a guest















              Required, but never shown

























              2 Answers
              2






              active

              oldest

              votes








              2 Answers
              2






              active

              oldest

              votes









              active

              oldest

              votes






              active

              oldest

              votes








              up vote
              4
              down vote



              accepted










              It seems you discovered the difference between a set of typing rules and an algorithm for type inference.



              Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. Their purpose is only to precisely define a mathematical relation $Gamma vdash t: tau$.



              Once we have such definition, we do not automatically get a type checking algorithm. That is, in general, there is no algorithm described by the rules which, given $Gamma,t,tau$, is able to test whether $Gamma vdash t: tau$ holds. (In some cases, such an algorithm could even fail to exist!)



              Similarly, we do not automatically obtain a type inference algorithm, which given $Gamma,t$ is able to find a related $tau$ (when it exists).



              The type checking/type inference algorithm must be devised independently.



              Now, it is true that in many cases the algorithms can follow the rules quite closely. The rule for non-recursive LET you mention is one nice example, since it is clear how to turn it into an algorithm. For recursive LETs, we are not that lucky.



              A typical strategy to type check/infer recursive LETs is to introduce a fresh type variable in the environment, and then perform type checking on the body while generating a set of constraints. For instance, consider this example



              let-rec f (x: int) = 1 + f(x) in f(0)


              We discover immediately that f : int -> ???. Let's introduce a fresh type variable R for the result, and say f : int -> R.



              We then type check 1 + f(x) assuming the environment f: int -> R , x: int.
              Here + is applied to arguments 1: int and f(x): R. Assuming + requires its arguments to be of the same type, this forces the constraint int = R.
              If + also returns the same type, we obtain another constraint int = R (redundant, in this case).



              Finally, we solve the constraints, discovering R = int.



              Note that in the general case we might be less lucky, since more complex types could be involved.



              let-rec f(x: int) = (2, fst(f(x-1)))


              Here, we discover f: int -> R, then we see that R must be a pair type R = A*B, then A=int (because of the 2). Moreover, we get f(x-1):R so fst(f(x-1)): A, hence B=A. We conclude f: int->(int*int).



              It is not trivial to generate these constraints, or to solve them (usually through a unification algorithm). In the scientific literature we can find several algorithms which perform this, but they are not obvious at first.






              share|cite|improve this answer



























                up vote
                4
                down vote



                accepted










                It seems you discovered the difference between a set of typing rules and an algorithm for type inference.



                Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. Their purpose is only to precisely define a mathematical relation $Gamma vdash t: tau$.



                Once we have such definition, we do not automatically get a type checking algorithm. That is, in general, there is no algorithm described by the rules which, given $Gamma,t,tau$, is able to test whether $Gamma vdash t: tau$ holds. (In some cases, such an algorithm could even fail to exist!)



                Similarly, we do not automatically obtain a type inference algorithm, which given $Gamma,t$ is able to find a related $tau$ (when it exists).



                The type checking/type inference algorithm must be devised independently.



                Now, it is true that in many cases the algorithms can follow the rules quite closely. The rule for non-recursive LET you mention is one nice example, since it is clear how to turn it into an algorithm. For recursive LETs, we are not that lucky.



                A typical strategy to type check/infer recursive LETs is to introduce a fresh type variable in the environment, and then perform type checking on the body while generating a set of constraints. For instance, consider this example



                let-rec f (x: int) = 1 + f(x) in f(0)


                We discover immediately that f : int -> ???. Let's introduce a fresh type variable R for the result, and say f : int -> R.



                We then type check 1 + f(x) assuming the environment f: int -> R , x: int.
                Here + is applied to arguments 1: int and f(x): R. Assuming + requires its arguments to be of the same type, this forces the constraint int = R.
                If + also returns the same type, we obtain another constraint int = R (redundant, in this case).



                Finally, we solve the constraints, discovering R = int.



                Note that in the general case we might be less lucky, since more complex types could be involved.



                let-rec f(x: int) = (2, fst(f(x-1)))


                Here, we discover f: int -> R, then we see that R must be a pair type R = A*B, then A=int (because of the 2). Moreover, we get f(x-1):R so fst(f(x-1)): A, hence B=A. We conclude f: int->(int*int).



                It is not trivial to generate these constraints, or to solve them (usually through a unification algorithm). In the scientific literature we can find several algorithms which perform this, but they are not obvious at first.






                share|cite|improve this answer

























                  up vote
                  4
                  down vote



                  accepted







                  up vote
                  4
                  down vote



                  accepted






                  It seems you discovered the difference between a set of typing rules and an algorithm for type inference.



                  Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. Their purpose is only to precisely define a mathematical relation $Gamma vdash t: tau$.



                  Once we have such definition, we do not automatically get a type checking algorithm. That is, in general, there is no algorithm described by the rules which, given $Gamma,t,tau$, is able to test whether $Gamma vdash t: tau$ holds. (In some cases, such an algorithm could even fail to exist!)



                  Similarly, we do not automatically obtain a type inference algorithm, which given $Gamma,t$ is able to find a related $tau$ (when it exists).



                  The type checking/type inference algorithm must be devised independently.



                  Now, it is true that in many cases the algorithms can follow the rules quite closely. The rule for non-recursive LET you mention is one nice example, since it is clear how to turn it into an algorithm. For recursive LETs, we are not that lucky.



                  A typical strategy to type check/infer recursive LETs is to introduce a fresh type variable in the environment, and then perform type checking on the body while generating a set of constraints. For instance, consider this example



                  let-rec f (x: int) = 1 + f(x) in f(0)


                  We discover immediately that f : int -> ???. Let's introduce a fresh type variable R for the result, and say f : int -> R.



                  We then type check 1 + f(x) assuming the environment f: int -> R , x: int.
                  Here + is applied to arguments 1: int and f(x): R. Assuming + requires its arguments to be of the same type, this forces the constraint int = R.
                  If + also returns the same type, we obtain another constraint int = R (redundant, in this case).



                  Finally, we solve the constraints, discovering R = int.



                  Note that in the general case we might be less lucky, since more complex types could be involved.



                  let-rec f(x: int) = (2, fst(f(x-1)))


                  Here, we discover f: int -> R, then we see that R must be a pair type R = A*B, then A=int (because of the 2). Moreover, we get f(x-1):R so fst(f(x-1)): A, hence B=A. We conclude f: int->(int*int).



                  It is not trivial to generate these constraints, or to solve them (usually through a unification algorithm). In the scientific literature we can find several algorithms which perform this, but they are not obvious at first.






                  share|cite|improve this answer














                  It seems you discovered the difference between a set of typing rules and an algorithm for type inference.



                  Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. Their purpose is only to precisely define a mathematical relation $Gamma vdash t: tau$.



                  Once we have such definition, we do not automatically get a type checking algorithm. That is, in general, there is no algorithm described by the rules which, given $Gamma,t,tau$, is able to test whether $Gamma vdash t: tau$ holds. (In some cases, such an algorithm could even fail to exist!)



                  Similarly, we do not automatically obtain a type inference algorithm, which given $Gamma,t$ is able to find a related $tau$ (when it exists).



                  The type checking/type inference algorithm must be devised independently.



                  Now, it is true that in many cases the algorithms can follow the rules quite closely. The rule for non-recursive LET you mention is one nice example, since it is clear how to turn it into an algorithm. For recursive LETs, we are not that lucky.



                  A typical strategy to type check/infer recursive LETs is to introduce a fresh type variable in the environment, and then perform type checking on the body while generating a set of constraints. For instance, consider this example



                  let-rec f (x: int) = 1 + f(x) in f(0)


                  We discover immediately that f : int -> ???. Let's introduce a fresh type variable R for the result, and say f : int -> R.



                  We then type check 1 + f(x) assuming the environment f: int -> R , x: int.
                  Here + is applied to arguments 1: int and f(x): R. Assuming + requires its arguments to be of the same type, this forces the constraint int = R.
                  If + also returns the same type, we obtain another constraint int = R (redundant, in this case).



                  Finally, we solve the constraints, discovering R = int.



                  Note that in the general case we might be less lucky, since more complex types could be involved.



                  let-rec f(x: int) = (2, fst(f(x-1)))


                  Here, we discover f: int -> R, then we see that R must be a pair type R = A*B, then A=int (because of the 2). Moreover, we get f(x-1):R so fst(f(x-1)): A, hence B=A. We conclude f: int->(int*int).



                  It is not trivial to generate these constraints, or to solve them (usually through a unification algorithm). In the scientific literature we can find several algorithms which perform this, but they are not obvious at first.







                  share|cite|improve this answer














                  share|cite|improve this answer



                  share|cite|improve this answer








                  edited Dec 8 at 9:23

























                  answered Dec 7 at 13:27









                  chi

                  11.4k1830




                  11.4k1830






















                      up vote
                      4
                      down vote













                      Typing rules are not "code". There is no "evaluation order". All the rule is saying is: if we're given some $t_{res}$ and $t_{var}$ (and $t$ and $tenv$ and ...) such that the first two equations hold, then we can conclude the bottom equation. How you come up with the $t_{res}$ and $t_{var}$ is out of scope and not specified.



                      That said, often we can read these types of rules as programs, but they are logic programs. In this context, the answer to your question is easy: you simply stick logic variables everywhere. Unification will handle the data transfer in whatever direction is needed.






                      share|cite|improve this answer

























                        up vote
                        4
                        down vote













                        Typing rules are not "code". There is no "evaluation order". All the rule is saying is: if we're given some $t_{res}$ and $t_{var}$ (and $t$ and $tenv$ and ...) such that the first two equations hold, then we can conclude the bottom equation. How you come up with the $t_{res}$ and $t_{var}$ is out of scope and not specified.



                        That said, often we can read these types of rules as programs, but they are logic programs. In this context, the answer to your question is easy: you simply stick logic variables everywhere. Unification will handle the data transfer in whatever direction is needed.






                        share|cite|improve this answer























                          up vote
                          4
                          down vote










                          up vote
                          4
                          down vote









                          Typing rules are not "code". There is no "evaluation order". All the rule is saying is: if we're given some $t_{res}$ and $t_{var}$ (and $t$ and $tenv$ and ...) such that the first two equations hold, then we can conclude the bottom equation. How you come up with the $t_{res}$ and $t_{var}$ is out of scope and not specified.



                          That said, often we can read these types of rules as programs, but they are logic programs. In this context, the answer to your question is easy: you simply stick logic variables everywhere. Unification will handle the data transfer in whatever direction is needed.






                          share|cite|improve this answer












                          Typing rules are not "code". There is no "evaluation order". All the rule is saying is: if we're given some $t_{res}$ and $t_{var}$ (and $t$ and $tenv$ and ...) such that the first two equations hold, then we can conclude the bottom equation. How you come up with the $t_{res}$ and $t_{var}$ is out of scope and not specified.



                          That said, often we can read these types of rules as programs, but they are logic programs. In this context, the answer to your question is easy: you simply stick logic variables everywhere. Unification will handle the data transfer in whatever direction is needed.







                          share|cite|improve this answer












                          share|cite|improve this answer



                          share|cite|improve this answer










                          answered Dec 7 at 8:44









                          Derek Elkins

                          8,91311729




                          8,91311729






























                              draft saved

                              draft discarded




















































                              Thanks for contributing an answer to Computer Science Stack Exchange!


                              • Please be sure to answer the question. Provide details and share your research!

                              But avoid



                              • Asking for help, clarification, or responding to other answers.

                              • Making statements based on opinion; back them up with references or personal experience.


                              Use MathJax to format equations. MathJax reference.


                              To learn more, see our tips on writing great answers.





                              Some of your past answers have not been well-received, and you're in danger of being blocked from answering.


                              Please pay close attention to the following guidance:


                              • Please be sure to answer the question. Provide details and share your research!

                              But avoid



                              • Asking for help, clarification, or responding to other answers.

                              • Making statements based on opinion; back them up with references or personal experience.


                              To learn more, see our tips on writing great answers.




                              draft saved


                              draft discarded














                              StackExchange.ready(
                              function () {
                              StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f101152%2flet-rec-recursive-expression-static-typing-rule%23new-answer', 'question_page');
                              }
                              );

                              Post as a guest















                              Required, but never shown





















































                              Required, but never shown














                              Required, but never shown












                              Required, but never shown







                              Required, but never shown

































                              Required, but never shown














                              Required, but never shown












                              Required, but never shown







                              Required, but never shown







                              Popular posts from this blog

                              數位音樂下載

                              When can things happen in Etherscan, such as the picture below?

                              格利澤436b