G. Allais 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 / 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 / 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 / tfix.agda

Created February 23, 2015 15:27

Descriptions

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 / 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 / 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 / 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 / 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 / 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 _`+_