Skip to content

Instantly share code, notes, and snippets.

View gallais's full-sized avatar

G. Allais gallais

301 followers · 168 following
View GitHub Profile
@gallais
gallais / ReverseVec.hs
Created January 27, 2015 12:15
Reverse Vec in Haskell without theorem proving
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
module ReverseVec where
data Nat = Z | S Nat
@gallais
gallais / phantom-type-alternative.hs
Last active August 29, 2015 14:15
Phantom.Alternative using phantom types
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
module Phantom.Alternative where
-- | universe of validation types
data Validated = Validated
data Unvalidated = Unvalidated
newtype FormData a = MkFD { pfd :: (Maybe String, String) }
@gallais
gallais / Unfold.hs
Created February 22, 2015 00:26
Unfold of a Fix
module Unfold where
newtype Fix f = InFix { outFix :: f (Fix f) }
unfoldFix :: Functor f => (s -> f s) -> s -> Fix f
unfoldFix node = go
where go = InFix . fmap go . node
data ListF a r = LNil | LCons a r
data TreeF a r = TNil | TLeaf a | TBranch r r
@gallais
gallais / tfix.agda
Created February 23, 2015 15:27
Descriptions
module tfix where
open import Data.Unit
open import Data.Product
data Desc : Set₁ where
arg : (A : Set) (d : A → Desc) → Desc
rec : (r : Desc) → Desc
ret : Desc
@gallais
gallais / Url.agda
Last active August 29, 2015 14:18
Url in Agda comments
module Url where
-- We usually start something about TT with the definition
-- of ℕ. So here we go:
data ℕ : Set where
z : ℕ
s : ℕ → ℕ
-- Now we want to embed a url in the comments. Why not use a
@gallais
gallais / Url.html
Last active August 29, 2015 14:18
Output of the script
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml"
><head
><title
>Url</title
><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
/><meta http-equiv="Content-Style-Type" content="text/css"
/><link href="Agda.css" rel="stylesheet" type="text/css"
/></head
><body
@gallais
gallais / Functor.agda
Created April 16, 2015 21:57
Functor constrained by a regular expression
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
module Data.Functor
(Alphabet : Set)
(_≤_ : (a b : Alphabet) → Set)
(_≟_ : (a b : Alphabet) → Dec (a ≡ b))
(_≤?_ : (a b : Alphabet) → Dec (a ≤ b))
where
@gallais
gallais / Examples.agda
Last active August 29, 2015 14:19
Functor Examples
module Data.Functor.Examples where
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Data.Char as Chr
open import lib.Char as Char
open import Data.String as Str
open import Data.List as List
open import Function
@gallais
gallais / Vector.agda
Last active August 29, 2015 14:21
Eta-short and Eta-expanded records not typechecked at the same type
-- Cf. this discussion for an explanation of what happens:
-- http://code.google.com/p/agda/issues/detail?id=1526
module Vector where
open import Data.Bool
open import Data.Nat
open import Data.Fin as Fin
open import Data.Unit
open import Data.Product
@gallais
gallais / RewriteQuote.agda
Created June 9, 2015 09:27
Quoting using REWRITE
module RewriteQuote where
open import Data.Bool
open import Data.Nat
open import Function
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
infixr 5 _`+_