Skip to content

Instantly share code, notes, and snippets.

🎯
Focusing

Jesús López-González jeslg

🎯
Focusing
Block or report user

Report or block jeslg

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
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.