edwinb

module Main
  
{- Divide x by y, as long as there is a proof that y is non-zero. The
   'auto' keyword on the 'p' argument means that when safe_div is called,
   Idris will search for a proof. Either y will be statically known, in
   which case this is easy, otherwise there must be a proof in the context.

   'so : Bool -> Type' is a predicate on booleans which only holds if the
   boolean is true. Essentially, we are making it a requirement in the type
   that a necessary dynamic type is done before we call the function -}

david-christiansen

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

divarvel

console.log("\033[39mRunning tests…");
function assertEquals(actual, expected, description) {
    if(typeof(actual) === "undefined") {
        console.error("\033[31m" + description + " not implemented\033[39m");
    } else {
        if(actual !== expected) {
            console.error("\033[31m" + description + " failed, expected " + expected + ", got " + actual + "\033[39m");
        } else {
            console.log(description + " \033[32m ok\033[39m");
        }

jozefg

module queue
import Data.Vect

-- Here's the port of the Liquid Haskell blog post on amortized
-- queues. The tricksy bit is that the "amortized" bit depends on
-- laziness. This means that while in the REPL (where Idris is lazy)
-- this is reasonably efficient. It compiles absolutely horribly
-- though because each time push or pop something we rotate the whole
-- damned thing.

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'.

jozefg

signature TYPEINFER =
sig
    type tvar =  int
    datatype monotype = TBool
                      | TArr of monotype * monotype
                      | TVar of tvar
    datatype polytype = PolyType of int list * monotype
    datatype exp = True
                 | False
                 | Var of int

rmoff

1. Download Instant Client:

• instantclient-basic-macos.x64-11.2.0.4.0.zip
• instantclient-sdk-macos.x64-11.2.0.4.0.zip
• instantclient-sqlplus-macos.x64-11.2.0.4.0.zip

2. Unzip and move to /opt

3. Create symlink

TheSeamau5

import Svg (Svg, circle, svg, g, line, text)
import Svg.Attributes (cx, cy, r, fill, stroke, strokeWidth, x, y, x1, x2, y1, y2, fontSize, style)
import Html
import Html.Attributes as Html

import Signal (Signal, map, foldp)
import DragAndDrop (mouseEvents, MouseEvent(..))
import List

--------------

chambart

type zero = unit
type 'a succ = unit -> 'a
type one = zero succ

type 'a plus_1 = 'a succ
type 'a plus_2 = 'a plus_1 plus_1
type 'a plus_4 = 'a plus_2 plus_2
type 'a plus_8 = 'a plus_4 plus_4

johnynek

object STRef {

  /**
   * Here is a container where we have a single "state thread" = ST.
   * When we run this thread of type ST[T] we get a result of type T.
   */
  sealed abstract class ST[+T] {
    def map[R](fn: T => R): ST[R] = flatMap(t => Const(fn(t)))
    def flatMap[R](fn: T => ST[R]): ST[R] = FlatMapped(this, fn)
  }