AndrasKovacs’s gists

AndrasKovacs / EvalApplyNBE.hs

Last active June 30, 2016 17:37

NbE for untyped lambda calculus is very similar to eval-apply environment machine evaluation

	{-# language LambdaCase #-}

	import Data.String
	import Data.HashMap.Lazy (HashMap, (!))
	import qualified Data.HashMap.Lazy as M

	data Term = Var !String \| !Term :$ !Term \| Lam !String !Term deriving (Show)

	instance IsString Term where
	fromString = Var . fromString

AndrasKovacs / SingNotes.hs

Created May 26, 2016 07:17

	{-# language DataKinds, PolyKinds, ScopedTypeVariables, UndecidableInstances,
	FlexibleInstances, FlexibleContexts, GADTs, TypeFamilies, RankNTypes,
	LambdaCase, TypeOperators, ConstraintKinds #-}

	import GHC.TypeLits
	import Data.Proxy
	import Data.Singletons.Prelude
	import Data.Singletons.Decide
	import Data.Constraint

AndrasKovacs / HVector.hs

Last active March 20, 2016 18:36

HLists backed by contiguous data

	{-# language
	FlexibleInstances, UndecidableInstances, MagicHash,
	PatternSynonyms, GADTs, TypeFamilies, ScopedTypeVariables, TypeOperators,
	DataKinds, ViewPatterns, RoleAnnotations, RankNTypes, ConstraintKinds #-}

	import GHC.Prim
	import Data.Vector (Vector)
	import qualified Data.Vector as V
	import Data.Proxy
	import Text.Show

AndrasKovacs / FinInj.agda

Last active January 23, 2016 15:48

Fin is injective - proven the relatively hard way without axiom K.

	{-# OPTIONS --without-K #-}

	-- the easy way is effectfully's brilliant heterogeneous equality solution:
	-- https://github.com/effectfully/random-stuff/blob/master/Fin-injective.agda

	open import Data.Fin hiding (_+_)
	open import Data.Nat
	open import Data.Nat.Properties.Simple
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary

AndrasKovacs / STLC.hs

Last active January 7, 2023 17:22

Lambda calculus on the type level with GHC 7.11.20151212.

	{-# LANGUAGE
	TypeInType, UndecidableInstances, TypeOperators, GADTs, TypeFamilies #-}

	import Data.Kind
	import GHC.Prim
	import Data.Proxy

	data Fun a b
	type a ~> b = Fun a b -> Type
	infixr 0 ~>

AndrasKovacs / Imp.hs

Created November 27, 2015 10:30

Small typesafe imperative embedded language

	{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, ScopedTypeVariables #-}
	{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, PartialTypeSignatures #-}
	{-# LANGUAGE UndecidableInstances #-}

	import Data.Singletons.Prelude
	import GHC.Exts
	import Data.List

	data NotInScopeError sym

AndrasKovacs / Hyperfunction.agda

Last active November 28, 2015 13:51

Hyperfunctions from Launchbury et al.'s http://arxiv.org/pdf/1309.5135.pdf, typed in Agda.

AndrasKovacs / IxFix.hs

Last active December 2, 2022 06:15

Example for recursion schemes for mutually recursive data

	{-# LANGUAGE
	UndecidableInstances, RankNTypes, TypeOperators, TypeFamilies,
	StandaloneDeriving, DataKinds, PolyKinds, DeriveFunctor, DeriveFoldable,
	DeriveTraversable, LambdaCase, PatternSynonyms, TemplateHaskell #-}

	import Control.Monad
	import Control.Applicative
	import Data.Singletons.TH

AndrasKovacs / FinSigma2.agda

Last active September 15, 2015 12:35

Alternative take on "finite sums of finite types are finite". This is much clearer and uses sensible lemmas (although it's not more succinct).


	open import Data.List renaming (map to lmap) hiding ([_])
	open import Relation.Binary.PropositionalEquality hiding ([_])
	open import Relation.Nullary
	open import Data.Empty
	open import Data.Product renaming (map to pmap)
	open import Data.Unit hiding (_≤_)
	open import Function
	open import Level renaming (suc to lsuc; zero to lzero)
	open import Data.Sum renaming (map to smap)

AndrasKovacs / Fin-neq-Nat.agda

Last active September 13, 2015 19:59

Nat is not equal to "Fin n" for any n.

	open import Data.Fin hiding (_<_; _≤_)
	open import Data.Nat
	open import Function
	open import Data.Product renaming (map to pmap)
	open import Data.List renaming (map to lmap)
	open import Relation.Binary.PropositionalEquality
	open import Data.Empty
	open import Relation.Nullary
	open import Relation.Binary
	open import Data.Sum renaming (map to smap)

András Kovács AndrasKovacs