{"size": 1621, "ext": "scrbl", "max_stars_repo_path": "redex-doc/redex/scribblings/long-tut/lab-tue-aft.scrbl", "max_stars_repo_name": "LiberalArtist/redex", "max_stars_repo_stars_event_min_datetime": "2018-07-29T04:13:52.000Z", "max_stars_repo_stars_event_max_datetime": "2022-02-14T16:11:17.000Z", "max_issues_repo_path": "redex-doc/redex/scribblings/long-tut/lab-tue-aft.scrbl", "max_issues_repo_name": "LiberalArtist/redex", "max_issues_repo_issues_event_min_datetime": "2017-08-25T20:26:37.000Z", "max_issues_repo_issues_event_max_datetime": "2022-02-26T17:48:40.000Z", "max_forks_repo_path": "redex-doc/redex/scribblings/long-tut/lab-tue-aft.scrbl", "max_forks_repo_name": "LiberalArtist/redex", "max_forks_repo_forks_event_min_datetime": null, "max_forks_repo_forks_event_max_datetime": null}
{"max_stars_count": 10, "max_issues_count": 15, "max_forks_count": null, "avg_line_length": 27.9482758621, "max_line_length": 102, "alphanum_fraction": 0.6255397903}
#lang scribble/manual

@(require "shared.rkt")

@; ---------------------------------------------------------------------------------------------------
@title[#:tag "lab-tue-aft"]{@bold{Lab} Type Checking}

@goals[
@item{subject reduction testing with @racket[trace]}
@item{typing judgments}
]

@common[]

In addition to @seclink["common.rkt"], you also want to @racket[require]
@seclink["tc-common.rkt"] for this lab. Furthermore, if you
copy code from @secref{tue-aft}, make sure to copy the tests and to adapt
the tests as you develop the machines.
		  
@; -----------------------------------------------------------------------------
@section[#:tag "lta" #:style 'unnumbered]{Exercises}

@exercise["ex:typing-trace"]{Develop a reduction system for which the
@racket[trace] expression from the lecture preserves types

@;%
@(begin
#reader scribble/comment-reader
(racketblock
(module+ test
  (traces ->
          (term (((lambda ((x (int -> int))) x) (lambda ((x int)) x)) 1))
          #:pred (lambda (e)
                   (judgment-holds (⊢ () ,e int)))))
))
@;%
}

@exercise["ex:typing"]{Extend @racket[TLambda] with syntax for the
following:
@;
@itemlist[

@item{additional numeric operators, say, multiplication, subtraction, and
division;} 

@item{@racket[let] expressions;}

@item{Boolean constants plus strict and and or operators as well as a
branching construct;}

@item{lists, specifically constructors and selectors (de-constructors);}

@item{explicitly recursive function definitions.}
]
Completing the above list is an ambitious undertaking, but do try to
complete at least two or three of these tasks.}
