AndrasKovacs’s gists

AndrasKovacs / ST.agda

Last active May 7, 2022 11:31

Computing ST monad in vanilla Agda


	open import Algebra
	open import Data.Bool
	open import Data.Empty
	open import Data.List
	open import Data.List.Properties
	open import Data.Nat
	open import Data.Product
	open import Data.Unit
	open import Function

AndrasKovacs / EffInference.hs

Last active May 14, 2018 09:50

Enhanced type inference for extensible effects with (limited) type reflection


	{-# language
	RankNTypes, GADTs, TypeInType, LambdaCase, TypeApplications,
	TypeOperators, StandaloneDeriving, TupleSections, EmptyCase,
	ScopedTypeVariables, TypeFamilies, ConstraintKinds,
	FlexibleContexts, MultiParamTypeClasses, AllowAmbiguousTypes,
	FlexibleInstances, DeriveFunctor, UndecidableInstances,
	NoMonomorphismRestriction #-}

	module EffInference where

AndrasKovacs / member-heq.agda

Last active February 23, 2017 08:55

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

	open import Data.List
	open import Data.Sum
	open import Relation.Binary.PropositionalEquality

	module _ (A : Set) where

	data _∈_ (a : A) : List A → Set where
	here : ∀ {as} → a ∈ (a ∷ as)

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.

András Kovács AndrasKovacs