Skip to content

Instantly share code, notes, and snippets.

View johnynek's full-sized avatar

P. Oscar Boykin johnynek

649 followers · 19 following
View GitHub Profile
@johnynek
johnynek / sort.bosatsu
Created November 22, 2019 19:54
quick sort in a total language. We use a Nat-like type to track the maximum number of steps, and show that we are always decreasing on the size of the list. This is a general strategy: compute first an upper bound of some kind using a Nat, then recurse carrying that counter through as proof that we will terminate.
# use this to track the maximum size of a list
enum Size: Z, S(prev: Size)
def size(list, acc):
recur list:
[]: acc
[_, *t]: size(t, S(acc))
def sort(ord: Order[a], list: List[a]) -> List[a]:
Order { to_Fn } = ord
@johnynek
johnynek / algebird_publish_error.txt
Created November 19, 2019 19:40
[info] Main Scala API documentation successful.
[info] published algebird-core_2.13 to /home/oscar/oss/algebird/target/sonatype-staging/0.13.6/com/twitter/algebird-core_2.13/0.13.6.part/algebird-core_2.13-0.13.6.jar.asc
[info] published algebird-core_2.13 to /home/oscar/oss/algebird/target/sonatype-staging/0.13.6/com/twitter/algebird-core_2.13/0.13.6.part/algebird-core_2.13-0.13.6.pom
[info] published algebird-core_2.13 to /home/oscar/oss/algebird/target/sonatype-staging/0.13.6/com/twitter/algebird-core_2.13/0.13.6.part/algebird-core_2.13-0.13.6-javadoc.jar.asc
[info] published algebird-core_2.13 to /home/oscar/oss/algebird/target/sonatype-staging/0.13.6/com/twitter/algebird-core_2.13/0.13.6.part/algebird-core_2.13-0.13.6-sources.jar
[info] published algebird-core_2.13 to /home/oscar/oss/algebird/target/sonatype-staging/0.13.6/com/twitter/algebird-core_2.13/0.13.6.part/algebird-core_2.13-0.13.6-sources.jar.asc
[info] published algebird-core_2.13 to /home/oscar/oss/algebird/target/sonatype-staging/0.13.6
@johnynek
johnynek / Dagify.scala
Created November 8, 2019 01:57
An algorithm to build a DAG out of any directed graph.
package com.stripe.unprotonated
import scala.collection.immutable.SortedSet
object Graph {
/**
* Build a DAG by merging individual nodes of type A into merged nodes of type SortedSet[A]
*/
final class Dagify[A: Ordering](seed: Set[A], val neighbors: A => Set[A]) {
@johnynek
johnynek / almosttailrec.scala
Last active May 13, 2024 02:10
A generalization of tail recursion for stack safety in scala
/*
* Consider a simple recursive function like:
* f(x) = if (x > 1) f(x - 1) + x
* else 0
*
* This function isn't tail recursive (it could be, but let's set that aside for a moment).
* How can we mechanically, which is to say without thinking about it, convert this into a stack safe recursion?
* An approach is to model everything that happens after the recursion as a continuation, and build up that
* continuation in a stack safe manner. Here is some example code:
*/
@johnynek
johnynek / RefMap.scala
Last active April 14, 2023 13:04
A wrapper on ConcurrentHashMap to use with cats.effect.Ref
package org.bykn.refmap
import cats.data.State
import cats.effect.Sync
import cats.effect.concurrent.Ref
import java.util.concurrent.ConcurrentHashMap
import cats.implicits._
/**
@johnynek
johnynek / dotty_list.scala
Last active January 12, 2020 13:43
Implementation of linked list using dotty features (opaque type, union types, extension methods, type lambda).
// unfortunately
// opaque type Fix[F[_]] = F[Fix[F]]
// won't work (no recursion in opaque type), but this implementation is safe, but scary due to asInstanceOf
object FixImpl {
type Fix[F[_]]
inline def fix[F[_]](f: F[Fix[F]]): Fix[F] = f.asInstanceOf[Fix[F]]
inline def unfix[F[_]](f: Fix[F]): F[Fix[F]] = f.asInstanceOf[F[Fix[F]]]
}
@johnynek
johnynek / map_module.scala
Last active March 13, 2019 16:20
A module based encoding of Map which keeps the ordering associated with the Map. Then we can talk about `mymod.Map` as a type, knowing that `mymod.ordering` is the ordering.
abstract class MapModule {
type K
def ordering: Ordering[K]
type Map[_]
def empty[V]: Map[V]
def updated[V](m: Map[V], key: K, v: V): Map[V]
def get[V](m: Map[V], key: K): Option[V]
def items[V](m: Map[V]): Stream[(K, V)]
def remove[V](m: Map[V], key: K): Map[V]
@johnynek
johnynek / Array covariance unsoundness.java
Created March 3, 2019 17:30
class B { }
class Main {
public static void main(String[] args) {
B strMain = Main.<String>cast("this is not a b");
System.out.println(strMain.toString());
}
public static <A extends Object> B cast(A a) {
B[] ary = new B[1];
@johnynek
johnynek / y.py
Last active March 3, 2019 16:21
Here is a port of this example y-combinator code: https://rosettacode.org/wiki/Y_combinator#Python except manually rewriting the lambdas into top-level functions accessing dictionaries to create closures.
def make_lambda(captured, fn, arity):
return {
"cap": captured,
"fn": fn,
"arity": arity,
"applied": [],
}
def apply_lambda(lam, arg):
app0 = lam["applied"]
@johnynek
johnynek / buildcart.scala
Last active December 16, 2018 16:39
Implementation of code from "Build Systems a la Carte", see: https://www.microsoft.com/en-us/research/publication/build-systems-la-carte/
package org.bykn.buildcart
import cats.{Alternative, Applicative, Id, Eq, Monad, Order, Traverse}
import cats.data.{Chain, Const, State}
import scala.collection.immutable.SortedSet
import cats.implicits._
object BuildCart {
trait Hash[A]