Sjoerd Visscher sjoerdvisscher

marcosh / NamedTypeclass.hs

Last active August 17, 2020 05:49

	{-# LANGUAGE AllowAmbiguousTypes #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TypeApplications #-}

	module NamedTypeclass where

	import Prelude hiding (Monoid, mempty, (<>))

basic-calculus / onekappa.hs

Last active March 29, 2021 08:41

One object kappa/zeta calculus, kind of like reflexive objects but also weird

	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE QuantifiedConstraints #-}
	import Prelude hiding (id, (.))
	import Control.Category
	import Control.Monad.State hiding (lift)

	class Category k => Terminal k where
	term :: k a ()

ant-arctica / LinearLogic.hs

Last active July 3, 2023 13:22

Implementing linear logic (double negation, ...) in linear haskell using linear-base

	{-# LANGUAGE BlockArguments #-}
	{-# LANGUAGE LambdaCase #-}
	{-# LANGUAGE LinearTypes #-}
	{-# LANGUAGE OverloadedRecordDot #-}
	{-# LANGUAGE NoImplicitPrelude #-}

	-- Quick demonstration that linear-base is enough to implement linear logic

	import Data.Array.Destination
	import Data.Array.Polarized.Pull

sjoerdvisscher / Endofunctors.hs

Last active August 11, 2025 12:27

Another go at implementing polynomial functors a la David Spivak

	{-# LANGUAGE GHC2021, GADTs, DataKinds #-}
	{-# LANGUAGE TypeData #-}
	module Endofunctors where

	import Control.Comonad (Comonad(..))
	import Control.Comonad.Cofree (Cofree(..))
	import Control.Monad (join, ap, void)
	import Control.Monad.Free (Free(..))
	import Data.Bifunctor (first, second, bimap)
	import Data.Functor.Day

sjoerdvisscher / Univ.hs

Last active January 14, 2025 14:27

Universal properties with plain Control.Category

	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE StandaloneKindSignatures #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE UndecidableInstances #-}

Lysxia / CoDebruijn.agda

Created February 17, 2025 20:00

CoDebruijn scoped syntax of untyped lambda calculus

	module CoDebruijn where

	open import Data.Product using (_×_; _,_; ∃-syntax)
	open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

	data Context : Set where
	O : Context
	1+_ : Context → Context

	data Singleton : Context → Set where