juanbono

-- The "Boolean" language from Types and Programming Languages, 3.5

-- Terms of the boolean language
data Term : Set where
  true false : Term
  if_then_else_ : Term → Term → Term → Term

-- A small-step semantics. Each constructor is a single reduction rule.
data _⟶_ : Term → Term → Set where
  e-IfTrue : ∀ {t₂ t₃} → if true then t₂ else t₃ ⟶ t₂

juanbono

General

http://blog.pluralsight.com/elixir-is-for-programmers #Idea assert, test http://www.q-lang.io/ #Definicion tipos como campos DB http://dlang.org/exception-safe.html #Alternativa try--except con scope http://floodyberry.com/noncryptohashzoo/ #Implementaciones de funcion HASH https://github.com/mikeash/MAObjCRuntime/blob/master/main.m #Mejor runtime obj-c, extendible https://github.com/jspahrsummers/libextobjc #Similar https://github.com/Midar/objfw/ #Implementacion de obj-c portable http://swtch.com/~rsc/regexp/regexp1.html #Mejor que regex http://swannodette.github.io/2013/07/12/communicating-sequential-processes/ #Fundamentos CSP

juanbono

Specification

Out Of The Tarpit

BOOM Analytics: Exploring Data-Centric, Declarative Programming for the Cloud

Dedalus: Datalog in Time and Space

Logic and Lattices for Distributed Programming

juanbono

#!/bin/bash

for i in *.mp4; do
    if [ ! -a "${i%.mp4}-fixed.mp4" ]; then
       ffmpeg -i "$i" -vcodec copy -ac 1 "${i%.mp4}-fixed.mp4"
    fi
done

juanbono

-- A port of: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html

{-# LANGUAGE DeriveFunctor #-}

module ABT where

import qualified Data.Foldable as Foldable
import Data.Foldable (Foldable)
import Data.Set (Set)
import qualified Data.Set as Set

juanbono

module Expr
import Data.Vect
import Data.Fin

data Expr : Nat -> Type where
  Var : Fin n -> Expr n
  Lam : Expr (S n) -> Expr n
  App : Expr n -> Expr n -> Expr n

data Closure : Type where

juanbono

Sometimes it would be nice if a type system could automatically "do it's best"
to restrict what a value will be. For example, the type `Bool` is the compiler
saying the value will either be `True` or `False`, but it doesn't know which.
What we want is the compiler to be able to be precise when possible, so instead
of always saying `Bool` (or "I don't know"), it could say `True`, `False`, or
`Bool`. This gist shows how Hindley Milner already has this capability that can
be exercised by using Church or Scott encodings of simple data types.

> {-# LANGUAGE RankNTypes #-}
> import qualified Data.Maybe as M

juanbono

module Classical where

open import Function using (_∘_; case_of_; id; _$_)
open import Data.Product using (_×_; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Bool
  using (Bool; true; false; not; if_then_else_)
  renaming (_∨_ to _b∨_; _∧_ to _b∧_)

juanbono

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where

juanbono

(* -*- mode: ocaml; -*- *)

module type FUNCTOR = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}

type var = string