kmicinski

#lang racket

;; (list-ref '(1 2 3) 0) => 1
;; (list-ref '(1 2 3) 1) => 2
;; (list-ref '(1 2 3) 2) => 3
;; assume i < (length l)
(define (list-ref l i)
  (if (equal? i 0)
      (first l)
      ;; should be a call to (list-ref (cdr l) ...)

kmicinski

#lang racket

(define l '(2 7 1))
(define l0 (cons 2 (cons 7 (cons 1 '()))))

(define (sum-list-of-length-3 l)
  (define x0 (first l))
  (define x1 (second l))
  (define x2 (third l))
  (+ x0 x1 x2))

kmicinski

Notes for our 2PM reading group tomorrow.  (Also CCing Darshana and Oliver, two DB collaborators of mine from UBuffalo) Very off-the-cuff thoughts here. I read this paper a few weeks ago and finally went through it again this afternoon to write up my thoughts.

Wow, very interesting paper. I am excited to discuss this. My highest level thoughts are that the restriction to circuits is doing a lot of the heavy lifting here, the authors say they are working on a compiler but it's not obvious to me that this won't hamper incrmentality in practice. Especially as you write richer programs that need to mix various data structures with varying concerns and space/materialization trade-offs.

PAPER TITLE: "DBSP: Automatic Incremental View Maintenance for Rich Query Languages"

SUMMARY

This paper presents a new approach to providing incremental view maintenance as a Rust library to a user. The high-level idea of incrementalization is being able to write programs that automatically work in terms of deltas--instead of ha

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]))