- 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
-
Unzip and move to /opt
-
Create symlink
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 -} |
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) |
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"); | |
} |
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. |
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'. |
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 |
Unzip and move to /opt
Create symlink
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 | |
-------------- |
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 |
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) | |
} |