AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

elizarov

import kotlin.coroutines.experimental.*
import kotlin.coroutines.experimental.intrinsics.*

fun main(args: Array<String>) {
    enumerate {
        if (flip("A")) {
            if (flip("B")) 1 else 2
        } else {
            if (flip("C")) 3 else if (flip("D")) 4 else 5
        }

rxwei

/// A type equality guarantee is capable of safely casting one value to a
/// different type. It can only be created when `S` and `T` are statically known
/// to be equal.
struct TypeEqualityGuarantee<S, T> {
  private init() {}

  /// Safely cast a value to the other type.
  func cast(_ value: T) -> S {
    return value as! S
  }

hediet

type StringBool = "true"|"false";


interface AnyNumber { prev?: any, isZero: StringBool };
interface PositiveNumber { prev: any, isZero: "false" };

type IsZero<TNumber extends AnyNumber> = TNumber["isZero"];
type Next<TNumber extends AnyNumber> = { prev: TNumber, isZero: "false" };
type Prev<TNumber extends PositiveNumber> = TNumber["prev"];

tylerneylon

license: mit

buzztaiki

sealed class Trampoline<A> {
    class More<A>(val fn: () -> Trampoline<A>): Trampoline<A>() {
        override fun toString() = "More"
    }
    class Done<A>(val a: A): Trampoline<A>() {
        override fun toString() = "Done($a)"
    }

    companion object {
        fun <A> run(fn: () -> Trampoline<A>): A = run(fn()).let {

steveash

import java.util.Random;

/**
 * Generates a sequence of pseudo-random numbers such that they never repeat. Can handle sequence sizes up to
 * length Int.MAX_VALUE. Will throw exceptions if you ask for more than that; maps the entire [0, Integer.MAX_VALUE]
 * range onto itself but in a random order
 * <link>http://preshing.com/20121224/how-to-generate-a-sequence-of-unique-random-integers/</link>
 */
public class PreshingRandomSequence {
    public static final int MAX_INT_PRIME = 2147483587;

bolot

<templateSet group="android">
  <template name="focvb" value="@Override&#10;public View onCreateView(LayoutInflater inflater, ViewGroup container, Bundle savedInstanceState) {&#10;    View view = inflater.inflate(R.layout.fragment_$END$, container, false);&#10;    ButterKnife.inject(this, view);&#10;    return view;&#10;}&#10;" description="Fragment onCreateView with ButterKnife" toReformat="true" toShortenFQNames="true">
    <context>
      <option name="JAVA_CODE" value="false" />
      <option name="JAVA_STATEMENT" value="false" />
      <option name="JAVA_EXPRESSION" value="true" />
      <option name="JAVA_DECLARATION" value="true" />
      <option name="JAVA_COMMENT" value="false" />
      <option name="JAVA_STRING" value="false" />
      <option name="COMPLETION" value="false" />

jbgi

import static java.lang.System.*;

import java.util.function.BiFunction;
import java.util.function.Function;

// Implementation of a pseudo-GADT in Java, translating the examples from
// http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf
// The technique presented below is, in fact, just an encoding of a normal Algebraic Data Type
// using a variation of the visitor pattern + the application of the Yoneda lemma to make it
// isomorphic to the targeted 'GADT'.

ksaua

// Let's say we have a gradle plugin. Now we want that gradle plugin project to actually use the exact plugin.
// There are probably multiple ways we can bootstrap this. One way is to build the jar, and use that, but that's boring.
// Here we show how we can have the plugin-project use the actual plugin we are building.

// :: We load the groovy script on runtime, only then are we able to apply the plugin
// Setup the groovy classpath. Start with our own files
def classpaths = [file('src/main/groovy').absolutePath, file('src/main/resources').absolutePath]
// The groovy script engine wants a string array
String[] classpathArray = classpaths.toArray(new String[classpaths.size()]);
// Start a groovy script engine with our classpaths