Skip to content

Instantly share code, notes, and snippets.

@jrslepak
jrslepak / sudoku.rkt
Created June 9, 2012 21:44
Sudoku solver
#lang racket
;;; problem-board and solved-board are included as examples
;;; (solve problem-board) should produce the same result as solved-board
(require rackunit)
;; A board is a 9-vector of 9-vectors (rows) of board-cells
(define (board? xs)
(define (row? r)
@jrslepak
jrslepak / curried.scrbl
Last active June 23, 2019 00:04
Scribble docs for curried functions?
#lang scribble/manual
This is a 3-argument curried function.
@defproc[(((lerp [lo number?])
[hi number?])
[alpha number?])
number?]{
Linear interpolation}
@jrslepak
jrslepak / inference.rkt
Last active May 24, 2017 19:04
Type inference in Typed Racket
#lang typed/racket
;;; Typed Racket version of Martin Grabmü̈ller's "Algorithm W Step by Step"
;;; http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.65.7733
;;; This is my first use of Typed Racket. I am looking to change this from
;;; following Haskell idiom to following Racket idiom.
;; An expression is a variable, a literal, an application,
@jrslepak
jrslepak / gist:5717099
Created June 5, 2013 20:37
define-union-language behavior examples
#lang racket
(require redex)
(define-language L1
(a integer)
(e variable-not-otherwise-mentioned
(* e e)))
(define-language L2
(b string)
@jrslepak
jrslepak / gist:5716442
Created June 5, 2013 19:19
Example proposed syntax for cross-language metafunctions in Redex
(define-language L1
(a integer)
(e variable-not-otherwise-mentioned))
(define-language L2
(b string)
(e integer))
(define-multilang-metafunction [L1 L2]
metafun-name : a L1:e -> b L2:e
@jrslepak
jrslepak / gist:5099883
Last active December 14, 2015 14:19
composition operations for testing type checker
; typing compose makes use of typechecker code for handling abstracted indices
(check-equal?
(judgment-holds
(type-of [] [] []
(I-λ [(s1 Shape) (s2 Shape) (s3 Shape)]
(T-λ [α β γ]
(A [] [(λ [(f (Array (S) ((Array s1 α) -> (Array s2 β))))
(g (Array (S) ((Array s2 β) -> (Array s3 γ))))]
(A [] [(λ [(x (Array s1 α))] (g (f x)))]))])))
type) type)
@jrslepak
jrslepak / gist:5095779
Last active December 14, 2015 13:48
typing compose
> (judgment-holds
(type-of []
[]
[]
(Λ [α β γ]
(A []
[(λ [(f 0 (Array (S) ((Array (S) α) -> (Array (S) β))))
(g 0 (Array (S) ((Array (S) β) -> (Array (S) γ))))]
(A [] [(λ [(x 0 (Array (S) α))] (g (f x)))]))]))
type)
@jrslepak
jrslepak / gist:5054161
Created February 28, 2013 04:22
Unexpected behavior from define-union-language -- the "two sublanguages" named in the error message are the same language
#lang racket
(require redex)
(define-language LBase
(e (+ e e)
number))
(define-extended-language L1 LBase
(e ....
(- e e)))
> (:print-type andmap)
(All (a c d b ...)
(case->
(-> (-> a c : d) (Listof a) c)
(-> (-> a b ... b c) (Listof a) (Listof b) ... b (U True c))))
> (λ ([a : Real]
[b : Symbol]
[c : Boolean]
#lang racket
(define (up-down x [so-far 1])
(if (equal? x so-far)
(displayln x)
(begin (displayln so-far)
(up-down x (add1 so-far))
(displayln so-far))))