Skip to content

Instantly share code, notes, and snippets.

Avatar

Łukasz Lew lukaszlew

  • Google
  • Mountain View
View GitHub Profile
View LambdaCubeIn100Lines.hs
-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
import Data.List (delete, union)
{- HLINT ignore "Eta reduce" -}
-- File mnemonics:
-- env = typing environment
-- vid = variable identifier in Bind or Var
-- br = binder variant (Lambda or Pi)
-- xyzTyp = type of xyz
-- body = body of Lambda or Pi abstraction
View zbaduk.sh
#!/bin/sh
# find unused filename
i=999
for i in $(seq 999 -1 100); do
new_file="${HOME}/go/problem-$i.png"
if [[ -e $new_file ]]; then
break
fi
file=$new_file
done
View gist:3fbd39e781927b38663977d359474418
HA 09:00 - 09:30 Deriving Via: or, How to Turn Hand-Written Instances into an Anti-pattern
HA 09:30 - 10:00 Generic Programming of All Kinds
HA 10:30 - 11:00 Type Variables in Patterns
ML 10:45 - 11:10 Rust Distilled: An Expressive Tower of Languages
ML 11:10 - 11:35 Generating Mutually Recursive Definitions
HA 11:30 - 12:00 Suggesting Valid Hole Fits for Typed-Holes (Experience Report)
HA 14:30 - 15:00 Coherent Explicit Dictionary Application for Haskell
ML 15:30 - 16:10 Programming with Abstract Algebraic Effects
@lukaszlew
lukaszlew / Closed.hs
Last active Jan 19, 2019
Another exposition of Edward's "Closed kinds aren't as closed as you'd think"
View Closed.hs
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language FlexibleInstances #-}
{-# language ScopedTypeVariables #-}
data Unit = U
class C (k :: Unit) where
get :: Int