philnguyen

class Convertible {α : Type} (u : α) (v : α) where
  ratio : Float

-- Reflexivity
instance : Convertible u u where
  ratio := 1

-- Symmetry
instance [sym : Convertible u v]: Convertible v u where
  ratio := 1 / sym.ratio

philnguyen

#lang typed/racket
(require bnf)

(Hint . ::= . (At [c : Char] [pos : Integer])
              (Present [c : Char] [but-not : Integer])
              (Absent [c : Char]))

(struct Accum ([pool : (Listof String)] [explored-letters : (Setof Char)]))

(: refine : Accum (Listof Hint) → Accum)

philnguyen

object Test {

  @JvmStatic
  fun main(args: Array<String>) {
    val strs = supplier("foo", "bar")
    val ints = supplier(1, 2)
    mergeSuppliers(strs, ints)
    val s = strs()[2] // boom!
  }

philnguyen

class Test {
  interface Supplier<T> { List<T> get(); }
 
  public static void main(String[] args) {
    Supplier<String> strs = supplier("foo", "bar");
    Supplier<Integer> ints = supplier(1, 2);
    mergeSuppliers(Arrays.asList(strs, ints));
    String s = strs.get().get(2); // boom!
  }
 

philnguyen

#lang racket/base

(require redex)

(define-language μ-Kanren
  ;; Syntax
  [#|Term    |# t ::= x () number (t t)]
  [#|Goal    |# g ::= (g ∨ g) (g ∧ g) (∃ (x ...) g) (↓ f t ...) (t ≡ t)]
  [#|Goal Abs|# f ::= (side-condition (name f any) (procedure? (term f)))]
  [#|Variable|# x ::= variable-not-otherwise-mentioned]

philnguyen

#lang racket

(require soft-contract/fake-contract)

(struct tzgap (starts-at offset-before offset-after) #:transparent)
(struct tzoffset (utc-seconds dst? abbreviation) #:transparent)
(struct tzoverlap (offset-before offset-after) #:transparent)

(define tz? (or/c string? exact-integer?))
(define system-tzid #:opaque)

philnguyen

#lang racket

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Syntactic Sugar
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; A proposition is a dependent contract whose range ignores the result
;; and only checks for the side-condition.
;; Termination is currently omitted.
(define-syntax-rule (∀ ([x c] ...) prop)

philnguyen

#lang racket/base

(module typed typed/racket/base
  (provide double)
  (define-type Increasing (([n : Natural]) . → . (Refine [a : Natural] (> a n))))
  (: double : Increasing → Increasing)
  ;; Modular type-checking of this module cannot eliminate:
  ;; - `(Refine [a : Natural] (> a n))` in `f`'s range
  ;; - `Natural` in `n`
  (define ((double f) n) (f (f n))))

philnguyen

#lang racket
(require termination)

(define (nondet) (- (random 1000) 500))
(define (nondet?) (> (random) 0.5))

;; Program with "ghost" states `d1`, `d2` tracking variable distances
(define (main* [x (nondet)] [y (nondet)] [z (nondet)])
  (printf "- init: ~a ~a ~a~n" x y z)
  (when (> y 0)

philnguyen

#lang racket/base

(require "../main.rkt")

(define (open-ack m n rec)
  (cond [(zero? m) (+ 1 n)]
        [(zero? n) (rec (- m 1) 1)]
        [else (rec (- m 1) (rec m (- n 1)))]))

(define close