pozorvlak

Here's where I understand the state of the art to be:

• In this INRIA tech report, Shapiro, Preguiça, Baquero and Zawirski (SPBZ) prove, amongst other things, that a sufficient condition for CRDTs to achieve eventual consistency on networks which may reorder and duplicate packets (which I'll call flaky networks, henceforth) is that
  1. the underlying datatype forms a semilattice,
  2. messages are full states,
  3. incoming messages are combined with the node's current state using the least-upper-bound operation in the semilattice.
• It's possible to relax condition 2 and still achieve eventual consistency over flaky networks by fragmenting the state into independent parts and transmitting updates to each part separately. For instance, in the G-Set CRDT (an add-only bitset) one can transmit only the index of the element to be added.
• In [these slides from a talk at Dagstuhl](http://www.dagstuhl.de/mat/Files/13/13081/13081.BaqueroCarlos.Sl

jmason

import com.yammer.metrics.Metrics;
import com.yammer.metrics.core.*;
import com.yammer.metrics.reporting.GraphiteReporter;
import com.yammer.metrics.reporting.SocketProvider;
import com.yammer.metrics.stats.Snapshot;

import java.io.IOException;
import java.util.concurrent.TimeUnit;

/**

relaxdiego

Follow these steps to install graphite on OS X Mavericks.

Prerequisites

• Homebrew
• Python 2.7
• Git

Install dependencies

Install Cairo and friends

tonymorris

using System;

namespace PureIO {
  /*
    C# does not have proper sum types. They must be emulated.

    This data type is one of 4 possible values:
    - WriteOut, being a pair of a string and A
    - WriteErr, being a pair of a string and A
    - readLine, being a function from string to A

jonsterling

(* It is not possible in Standard ML to construct an identity type (or any other
 * indexed type), but that does not stop us from speculating. We can specify with
 * a signature equality should mean, and then use a functor to say, "If there
 * were a such thing as equality, then we could prove these things with it."
 * Likewise, we can use the same trick to define the booleans and their
 * induction principle at the type-level, and speculate what proofs we could
 * make if we indeed had the booleans and their induction principle.
 *
 * Functions may be defined by asserting their inputs and outputs as
 * propositional equalities in a signature; these "functions" do not compute,

bobatkey

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system:

copumpkin

module RuntimeTypes where

open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All

chrisdone

Typing Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology

chrisdone

Basic unit type:

λ> replTy "()"
() :: ()

Basic functions:

karpathy

"""
Minimal character-level Vanilla RNN model. Written by Andrej Karpathy (@karpathy)
BSD License
"""
import numpy as np

# data I/O
data = open('input.txt', 'r').read() # should be simple plain text file
chars = list(set(data))
data_size, vocab_size = len(data), len(chars)