AndrasKovacs’s gists

AndrasKovacs / lzw.hs

Created March 14, 2015 17:55

LZW

	import Data.Maybe
	import Data.Char
	import Data.List

	dictionary :: [String]
	dictionary = [[chr x] \| x <- [0..127]]

	encode :: String -> [Int]
	encode [] = []
	encode (x:xs) = go dictionary [x] xs where

AndrasKovacs / GameSearch.hs

Created March 5, 2015 14:15

game tree search notes

	{-# LANGUAGE
	LambdaCase, NoMonomorphismRestriction,
	RankNTypes, ScopedTypeVariables,
	TupleSections, GADTs, FlexibleContexts,
	ViewPatterns, GeneralizedNewtypeDeriving #-}

	import Data.List
	import Data.List.Split
	import Data.Ord
	import Control.Lens

AndrasKovacs / PredSystemF.agda

Last active June 16, 2017 08:36

Another shot at System F with predicative instantiation. This time it's over a small closed universe and it's vastly simpler to implement. Inspired by Conor McBride's "Outrageous but Meaningful Coincidences".


	open import Function
	open import Data.Nat
	open import Data.Fin
	open import Data.Empty
	open import Data.Unit
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary
	open import Data.Product
	open import Data.Vec hiding (_∈_; module _∈_)

AndrasKovacs / AppendAssoc.hs

Last active August 29, 2015 14:12

Lifted list append is associative

	{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, GADTs, TypeFamilies #-}

	import Data.Type.Equality

	type family (++) (xs :: []) (ys :: []) where
	'[] ++ ys = ys
	(x ': xs) ++ ys = x ': (xs ++ ys)

	data SList (xs :: [*]) where
	Nil :: SList '[]

AndrasKovacs / STLC_with_vars.agda

Last active August 29, 2015 14:06

STLC in Agda, but with string variables and shadowing, instead of de Bruijn.

	open import Data.String
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary.Decidable
	open import Function
	open import Data.List
	open import Data.Product
	open import Relation.Nullary
	open import Data.Unit hiding (_≟_)
	open import Data.Empty
	open import Data.Bool hiding (_≟_)

AndrasKovacs / Perm.agda

Last active April 5, 2020 09:56

Permutation relation in Agda. In the indiuctive definition we have insertions on both sides, as opposed to one side. This makes the transitivity proof *horrible* (or at least I couldn't do better).


	open import Data.List
	open import Data.Nat
	open import Relation.Binary.PropositionalEquality
	open import Function
	open import Data.Product
	open import Data.Sum

	data _▶_≡_ {A : Set}(x : A) : List A → List A → Set where
	here : ∀ {xs} → x ▶ xs ≡ (x ∷ xs)

AndrasKovacs / Uniplate1.hs

Last active August 29, 2015 14:05

Two flavors of uniplate for indexed types.

	-- Lens style ----------------------

	-- Kudos for circed for holes and contexts in lens-style: http://stackoverflow.com/questions/25393870/how-can-holes-and-contexts-be-implemented-for-higher-kinded-types-in-a-lens-styl


	{-# LANGUAGE GADTs, RankNTypes, PolyKinds, StandaloneDeriving, ScopedTypeVariables #-}

	import Control.Applicative
	import Control.Monad.Identity

AndrasKovacs / ZipWithN.hs

Last active August 29, 2015 14:05

Polyvariadic zipWith.

	{-# LANGUAGE
	FlexibleInstances,
	MultiParamTypeClasses,
	UndecidableInstances,
	IncoherentInstances, -- GHC 7.10 can do with only Overlapping
	TypeFamilies #-}

	class ZipWithN f t where
	zipWithN' :: [f] -> t

AndrasKovacs / ListMonad.agda

Last active August 29, 2015 14:05

List is a monad.


	open import Data.List
	open import Function
	open import Relation.Binary.PropositionalEquality
	open import Data.Product
	open import Algebra
	module LM {a}{A : Set a} = Monoid (monoid A)

	infixr 5 _>>=_
	_>>=_ : ∀ {a b}{A : Set a}{B : Set b} → List A → (A → List B) → List B

AndrasKovacs / SystemF.agda

Last active June 30, 2019 21:11

Embedding of predicative polymorphic System F in Agda.


	open import Function
	open import Data.Nat hiding (_⊔_)
	open import Data.Fin renaming (_+_ to _f+_)
	open import Data.Unit
	open import Relation.Binary.PropositionalEquality
	open import Data.Product
	open import Data.Sum
	open import Data.Vec
	open import Data.Vec.Properties

András Kovács AndrasKovacs