Skip to content

Instantly share code, notes, and snippets.

🎯
Focusing

Jesús López-González jeslg

View GitHub Profile
@jeslg
jeslg / eff.hs
Created Jun 26, 2018
Experiments with transformers-eff
View eff.hs
{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances #-}
import Control.Effect
import Control.Effect.Environment
import Control.Effect.Exception
import Control.Monad.Reader hiding (ask)
import Control.Monad.State
import Control.Monad.Free
-- The effect is explicit in the resulting type
View safetraversal.v
Require Import Coq.Init.Nat.
Require Import Coq.Strings.String.
Require Import Coq.Vectors.VectorDef.
Open Scope string_scope.
Open Scope nat_scope.
(* Traversal definition and methods *)
@jeslg
jeslg / .sbtrc
Created May 10, 2018
SBT alias for Spark Intro
View .sbtrc
# SESSION4-SPARK
# ALL
alias test-sparkintro=;testOnly org.hablapps.sparkintro.test.*
# SECTIONS
alias sparkintro-intro=;testOnly org.hablapps.sparkintro.templates.Intro
alias sparkintro-core=;testOnly org.hablapps.sparkintro.templates.CoreRDDs
@jeslg
jeslg / preview-set.txt
Created May 7, 2018
Affine pointfree preview-set law
View preview-set.txt
Affine
======
pre1 : A -> B + 1
set1 : A x B -> A
pre2 : B -> C + 1
set2 : B x C -> B
View induction.v
Fixpoint times2 (n : nat) : nat :=
match n with
| 0 => 0
| S n => S (S (times2 n))
end.
Fixpoint even (n : nat) : bool :=
match n with
| 0 => true
| S n => negb (even n)
@jeslg
jeslg / AffineSetoid.v
Last active Apr 30, 2018
Affine proof where [setoid_rewrite] fails.
View AffineSetoid.v
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Generalizable All Variables.
(* Subrelations to enable [setoid_rewrite] in general settings *)
Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
: subrelation (pointwise_relation A RB) eq.
@jeslg
jeslg / Monoid.v
Created Apr 26, 2018
`setoid_rewrite` fails in pattern matching scenario
View Monoid.v
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Generalizable All Variables.
Class Monoid (m : Type) :=
{ mzero : m
; mappend : m -> m -> m
}.
@jeslg
jeslg / University.scala
Created Apr 24, 2018
Toying around with different repository configurations
View University.scala
package org.hablapps
package university
import scalaz._, Scalaz._
case class University(name: String, departs: Map[String, Department])
case class Department(budget: Double)
object UniversityManyDep extends App {
@jeslg
jeslg / Lens.v
Last active Jan 15, 2018
Proof that very well-behaved lens is closed under composition.
View Lens.v
(* Lens and compose definitions *)
Record lens (S A : Type) := {
get : S -> A;
put : S -> A -> S }.
Definition compose {S A B : Type} (ln1 : lens S A) (ln2 : lens A B) : lens S B :=
{| get := fun (s : S) => ln2.(get A B) (ln1.(get S A) s);
put := fun (s : S) (b : B) => ln1.(put S A) s (ln2.(put A B) (ln1.(get S A) s) b) |}.
@jeslg
jeslg / LensComposition.md
Last active Jan 5, 2018
Very well-behaved lens composition is closed
View LensComposition.md

Lens Composition Proofs

Structure

type Lens s a = (GET :: s -> a, PUT :: s -> a -> s)

Lens Laws

  • GetPut: PUT s (GET s) => s
  • PutGet: GET (PUT s a) => a
You can’t perform that action at this time.