Maxime DIDIER madidier

madidier / Either-hof.agda

Last active November 25, 2024 11:14

Sum type encoding and catamorphism of "Either" in various languages and approaches

	-- I haven't been able to actually run the program (broken archlinux packages), but it typechecks

	open import Data.String
	open import Function
	open import IO.Primitive

	Either : Set → Set → Set₁
	Either l r = {a : Set} → (l → a) → (r → a) → a

	Left : { l r : Set } → l → Either l r

madidier / Freegram.hs

Created November 16, 2016 23:32

Johachim Breitner's Applicative showcase, free applicative version

	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE LambdaCase #-}

	module Freegram where

	import Bnf
	import Parser

	import Control.Applicative.Free.Final
	import Data.Maybe (catMaybes)

madidier / Tabulata.hs

Last active October 22, 2016 11:55

A general DSL for consuming structured tabular data (i.e. wide CSVs, XLSXs...)

	{-# LANGUAGE BangPatterns #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE LambdaCase #-}
	{-# LANGUAGE OverloadedStrings #-}

	module Tabulata
	( -- * Types
	Fields
	, Range