kmicinski

--                   ------ u           
--                      P              
--                   ------ ∧I          ------- k
--                    P × P               R
--                   ------------- ∨I2  ------- ∨I₁
--                    (R ⊎ (P × P))    (R ⊎ (P × P)) 
--     k ----------  -------------------------------
--         (P ⊎ R)           (R ⊎ (P × P))
--   ∨Eᵘᵐ ----------------------------------
--           (R ⊎ (P × P))

kmicinski

module foo where
open import Relation.Nullary
open import Data.Sum.Base
import Data.String as String
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_;_^_)

data _≤_ : ℕ → ℕ → Set where

kmicinski

#lang racket

;; Class 1 -- Type Checking
;;
;; In this exercise we will check fully-annotated terms
;; In the next project we will look at synthesis

;; We will build a type system based on the
;; Simply-Typed λ-calculus (STLC)

kmicinski

;; Using the type rules on the practice exam
;;
;; Write typing derivations of the following judgements.
;; If there is no possible typing derivation, explain
;; the issue.

{ x : num → (bool → bool), z : bool } ⊢ ((x 3) z) : bool

{ z : bool } ⊢ ((lambda (x : bool → num) (x z)) (lambda (y : bool) z)) : num

kmicinski

(define (synthesize-type env e)
  (match e
    ;; Literals
    [(? integer? i) 'int]
    [(? boolean? b) 'bool]
    ;; Look up a type variable in an environment
    [(? symbol? x) (hash-ref env x)]
    ;; Lambda w/ annotation
    [`(lambda (,x : ,A) ,e)
     ;; I know the type is A -> B, where B is the type of e when I

kmicinski

#lang racket

(define (op? op)
  (member op '(+ - * / cons car cdr = equal? length)))

(define (op->racket op)
  (eval op (make-base-namespace))) ;; the *only* acceptable use of Racket's `eval` in this project

;; First attempt
(define (eval-a e env)

kmicinski

#lang racket

(define (expr? e)
  (match e
    [(? number? n) #t]
    [(? symbol? x) #t]
    [`(λ (,(? symbol? x)) ,(? expr? e)) #t]
    [`(,(? expr? e0) ,(? expr? e1)) #t]
    [_ #f]))

kmicinski

#lang racket

;; general direct-style recursive template over lists
#;(define (my-function lst)
  (if (empty? lst)
      'base-case
      (let ([result-from-rest-of-list (my-function (rest lst))]
            [first-list (first lst)])
        (f first-list result-from-rest-of-list))))

kmicinski

#lang racket

;; omega term = 
;; ((lambda (x) (x x)) (lambda (x) (x x)))
;; (x x) [ x ↦ (lambda (x) (x x)) ] =
;; ((lambda (x) (x x)) (lambda (x) (x x)))

;; there are two options
'((lambda (x) (lambda (y) y)) ((lambda (x) (x x)) (lambda (x) (x x))))

kmicinski

#lang racket

;; λ-calculus expressions
(define (expr? e)
  (match e
    [(? symbol? x) #t] ;; variables
    [`(λ (,(? symbol? x)) ,(? expr? e-body)) #t] ;; λ abstractions
    [`(,(? expr? e-f) ,(? expr? e-a)) #t] ;; applications
    [_ #f]))