Skip to content

Instantly share code, notes, and snippets.

@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}
> (: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))))
#lang rackmora
(def count10 (R_iota [10]))
(R_iota [10])
(fn ((top 0))
(unbox counting count10 1))
(def sum
(fn ((top 0))
#lang slideshow
(require (planet jaymccarthy/slideshow-latex))
(latex-dpi 300)
(add-preamble #<<latex
\usepackage{amsmath}
latex
)
@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)