Skip to content

Instantly share code, notes, and snippets.

View juanbono's full-sized avatar
:shipit:

Juan Bono juanbono

:shipit:
View GitHub Profile
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
juanbono / hm_scott.lhs
Created July 4, 2016 10:42 — forked from stelleg/hm_scott.lhs
Hindley Milner + Scott Encoding Musings
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
juanbono / Classical.agda
Created July 10, 2016 18:52 — forked from laMudri/Classical.agda
Double negation embedding
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
juanbono / UntypedLambda.agda
Created July 10, 2016 19:02 — forked from gallais/UntypedLambda.agda
Interpreting the untyped lambda calculus in Agda
{-# OPTIONS --copatterns #-}
module UntypedLambda where
open import Size
open import Function
mutual
data Delay (A : Set) (i : Size) : Set where
@juanbono
juanbono / abt
Created July 12, 2016 15:00 — forked from neel-krishnaswami/abt
Abstract binding trees implementation
(* -*- 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
@juanbono
juanbono / gist:cc3bf9e88a11282be54bb7caf4dca042
Created July 31, 2016 20:10 — forked from tausen/gist:4261887
pthread, sem_wait, sem_post example
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <pthread.h>
#include <unistd.h>
#include <semaphore.h>
sem_t semaphore;
void threadfunc() {
@juanbono
juanbono / recuperatorioFuncional2016.hs
Last active December 9, 2016 19:10
Recuperatorio del Paradigma Funcional, año 2016
-- Enlace: https://docs.google.com/document/d/1TTaIK1kPWuhkvWnnlf9SZSodBtSXhiewOAex4wNtSps
{-
data Raton = UnRaton String Float Float [Enfermedad] deriving
(Show, Eq)
-}
-- Se puede declarar el tipo de dato de esta forma, asi nos ahorramos
-- declarar manualmente las funciones para obtener cada componente de
-- un raton.
data Raton = UnRaton {
@juanbono
juanbono / findRaspberryPI-IP.txt
Last active October 3, 2017 04:14
Comando para encontrar la ip de la raspberry usando nmap
# Si es a traves de internet (por ejemplo, tengo la raspberry conectada directamente al modem o con wifi):
sudo nmap -sP 192.168.1.0/24 | awk '/^Nmap/{ip=$NF}/B8:27:EB/{print ip}'
# Si tengo conectada la rpi conectada a mi pc mediante Ethernet:
# 1. Cambiar la conexión ethernet, para que comparta internet con los demas equipos.
# 2. Usar ifconfig para saber cual es la dirección de broadcast de la interfaz Ethernet
# 3. Utilizar nmap de forma similar al otro caso, pero con la direccción de broadcast de Ethernet:
sudo nmap -sP 10.42.0.255/24 | awk '/^Nmap/{ip=$NF}/B8:27:EB/{print ip}'
@juanbono
juanbono / ngrxintro.md
Created November 2, 2016 01:12 — forked from btroncone/ngrxintro.md
A Comprehensive Introduction to @ngrx/store - Companion to Egghead.io Series

#Comprehensive Introduction to @ngrx/store By: @BTroncone

Also check out my lesson @ngrx/store in 10 minutes on egghead.io!

Update: Non-middleware examples have been updated to ngrx/store v2. More coming soon!

Table of Contents

@juanbono
juanbono / new-gplv3-full-project.hsfiles
Created January 9, 2017 05:42 — forked from queertypes/new-gplv3-full-project.hsfiles
Haskell Stack template: GPL-3, doctests, hlint, many other goodies
{-# START_FILE {{name}}.cabal #-}
name: {{name}}
version: 0.1.0.0
synopsis: Initial project template from stack
description: Please see README.md
license: GPL-3
license-file: LICENSE
author: {{author-name}}{{^author-name}}Author name here{{/author-name}}
maintainer: {{author-email}}{{^author-email}}[email protected]{{/author-email}}
copyright: {{copyright}}{{^copyright}}{{year}}{{^year}}2017{{/year}} {{author-name}}{{^author-name}}Author name here{{/author-name}}{{/copyright}}