corajr

def add_to_list(w, in_boxes):
    if len(in_boxes) == 0:
        return [1.0-w]
    else:
        boxes = in_boxes[:]
        max_box = max(boxes)
        if w >= max_box and w != 0.0:
            boxes.append(1.0-w)
            return boxes
        else:

corajr

The problem statement, for reference:

Consider a datatype definition that introduces numeric lists as the sum of two variants: nempty and ncons. This defines a new type (nlist), and each constructor (such as ncons) creates a value of that type. As a result, however, selectors (such as nfirst) cannot statically determine whether or not they have been given the correct variant of the datatype, and must rely on a check from the run-time system. >

corajr

module Example where

{-@ divide' :: Int -> {v: Int | v != 0} -> Int @-}
divide' :: Int -> Int -> Int
divide' n d = n `div` d

-- liquid knows we're lying!
{-@ maybeZero :: Bool -> {v: Int | v != 0} @-}
maybeZero :: Bool -> Int
maybeZero True = 1

corajr

let withDefault (defaultVal: 'a, x : 'a option) = 
    match x with
    | Some(xVal) -> xVal
    | None -> defaultVal

corajr

module Nat where

import Prelude hiding (succ)
import Control.Monad (forM_)

data Even = Zero | EvenSucc Odd
         deriving (Show, Eq)

data Odd = OddSucc Even
         deriving (Show, Eq)

corajr

class MyData { ... }
class YourData { ... }

abstract class Generic<T> {
    public T tObject;

    // constructor takes a T, whatever it is
    public Generic(T tObject) { this.tObject = tObject; }

    public abstract T giveMeTheT();

corajr

eg() {
    tmpfile=$(mktemp -t gist)
    filename=${1:-$(basename $tmpfile)}
    $EDITOR $tmpfile
    if [ -s $tmpfile ]
    then
        gist -c -f $filename $tmpfile
    fi
    rm -f $tmpfile
}

corajr

import java.util.*;

class MapDiff {
    public static void main(String[] args) {
        Map<String, Integer> m1 = new HashMap<String, Integer>();
        m1.put("a", 1);
        m1.put("b", 2);
        m1.put("c", 3);

        Map<String, Integer> m2 = new HashMap<String, Integer>();

corajr

module ClosestToZero where

closestToZero :: [Int] -> Maybe Int
closestToZero [] = Nothing
closestToZero xs = Just $ foldl1 f xs
  where f x y = case compare (abs x) (abs y) of
                  LT -> x
                  EQ -> abs x
                  GT -> y

corajr

module Data.Tree where

import Data.List (sortBy)
import Data.Ord (comparing)

data Tree a = Tip | Node a (Tree a) (Tree a)
            deriving (Show, Eq)

-- x, y
type Coords = (Int, Int)