mankyKitty

-- Working through the Yorgey lectures on Applicatives for Haskell and trying to work out the homework...

-- A parser for a value of type a is a function which takes a String
-- represnting the input to be parsed, and succeeds or fails; if it
-- succeeds, it returns the parsed value along with the remainder of
-- the input.
newtype Parser a = Parser { runParser :: String -> Maybe (a, String) }

-- For example, 'satisfy' takes a predicate on Char, and constructs a
-- parser which succeeds only if it sees a Char that satisfies the

mankyKitty

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

data Nat = Z | S Nat

plus :: Nat -> Nat -> Nat
plus Z n = n
plus n Z = n

mankyKitty

Theorem identity_fn_applied_twice : 
  forall (f : bool -> bool),
    (forall (x : bool), f x = x) -> forall (b : bool), f (f b) = b.
Proof.
  intros f x b. (* Introduce our parameters *)
  destruct b as [| b']. (* destruct b for possible values of b' <-- I don't use this and it worries me *)
  rewrite -> x. (* rewrite f (f true) = true to f true = true *)
  rewrite -> x. (* rewrite f true = true to true = true *)
  reflexivity. (* solve the first subgoal above *)
  rewrite -> x. (* rewrite f (f false) = false to f false = false *)

mankyKitty

{-# LANGUAGE DeriveDataTypeable #-}

module Main where

import Data.Typeable
import Data.Data
import Data.List

import Control.Monad.State
import Data.Generics.Uniplate.Data

mankyKitty

(** **** Exercise: 2 stars (andb_eq_orb) *)
(** Prove the following theorem.  (You may want to first prove a
    subsidiary lemma or two.) *)

Theorem andb_b_c :
  forall (b c : bool),
    b = c -> andb b c = b.
Proof.
  intros b c H.
  destruct H. 

mankyKitty

    <?php
    
      try {
        migrate_instrument_start('destination import', TRUE);
        $ids = $this->destination->import($this->destinationValues, $this->sourceValues);
        migrate_instrument_stop('destination import');
        if ($ids) {
          $this->map->saveIDMapping($this->sourceValues, $ids,
            $this->needsUpdate, $this->rollbackAction,
            $data_row->migrate_map_hash);

mankyKitty

<?php
function relative_uri_rewrite($search_pattern, $rewrite_pattern, $uri) {
  if (count($search_pattern) == 0 || count($original) == 0) {
    return FALSE;
  }

  $pieces_of = function($p) {
    return explode('/', $p);
  };

mankyKitty

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Prelude hiding (first)

import Control.Applicative
import Data.Text (Text)
import qualified Data.Text as T
import Control.Monad.Trans.Either
import Control.Error ((??))

mankyKitty

Maybe = (v,isEmpty) ->
  `protected this.value = v`
  @isEmpty = isEmpty
  return

Maybe.Nothing = new Maybe(null, true)

Maybe.prototype.bind = (f) ->
  if @isEmpty then new Maybe.Nothing
  else new Maybe(f(@value))

mankyKitty

2:48 PM <Jeanne-Kamikaze> physically-based shading in modern game engines: when you add an animated character, you're back to 1970
2:49 PM <Jeanne-Kamikaze> I suppose that would make a good tweeter post
2:49 PM <edwardk> Jeanne-Kamikaze: =)
2:49 PM <Jeanne-Kamikaze> *twitter
2:49 PM <Jeanne-Kamikaze> see, I don't even know how to spell that shit xD
2:50 PM <Jeanne-Kamikaze> I still find it so ridiculous
2:53 PM <Jeanne-Kamikaze> alright, there goes my little contribution to this mindless world of 140 chars broadcasting
2:53 PM <Jeanne-Kamikaze> I mean, this whole 140 limit is just an evil scheme from the system to make the population even more dumb that it is now
2:54 PM <Jeanne-Kamikaze> it's like 1984: you remove words from the language, and suddenly people cannot communicate their ideas simply because they don't have the word for it
2:54 PM <Jeanne-Kamikaze> so the 140 chars limit forces people to oversimplify and summarise their ideas to the point where what you're saying is just plain bullshit