Skip to content

Instantly share code, notes, and snippets.

@sjoerdvisscher
sjoerdvisscher / CalcComp.hs
Created Aug 25, 2021
Calculating Dependently-Typed Compilers
View CalcComp.hs
-- https://icfp21.sigplan.org/details/icfp-2021-papers/21/Calculating-Dependently-Typed-Compilers-Functional-Pearl-
{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, TypeApplications, KindSignatures, ScopedTypeVariables #-}
import Control.Applicative
import Data.Kind
import Data.Type.Equality
type family (a :: Bool) || (b :: Bool) :: Bool where
'False || b = b
'True || b = 'True
@sjoerdvisscher
sjoerdvisscher / Uny.hs
Created Apr 30, 2021
Uny, build small datatypes with algebraic expressions
View Uny.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
View Rec.hs
{-# LANGUAGE DerivingStrategies, DerivingVia, TypeOperators, DataKinds,
DeriveGeneric #-}
module Rec where
import SameRepAs
import GHC.Generics ( Generic )
import qualified Data.Monoid as M
View HRecord.hs
{-# LANGUAGE StandaloneKindSignatures, DataKinds, DerivingStrategies,
TypeFamilies, GeneralizedNewtypeDeriving, DeriveGeneric,
TypeOperators, UndecidableInstances,
TypeApplications, ScopedTypeVariables,
FlexibleContexts, ConstraintKinds #-}
module HRecord where
import Data.Kind ( Type )
import GHC.Generics
View Rec.hs
{-# LANGUAGE DerivingStrategies, DerivingVia, TypeOperators, DataKinds,
DeriveGeneric #-}
module Rec where
import SameRepAs
import GHC.Generics ( Generic )
import qualified Data.Monoid as M
View LinearStateMonad.hs
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE QualifiedDo #-}
import Prelude.Linear hiding (partition)
import qualified Control.Functor.Linear as Linear
import Control.Functor.Linear (State, state, execState, pure)
import qualified Data.Array.Mutable.Linear as Array
@sjoerdvisscher
sjoerdvisscher / jules.hs
Created Feb 6, 2021
Van Laarhoven versions of Jules Hedges' stochastic lenses
View jules.hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
import Data.Coerce (coerce)
import Data.Functor.Compose (Compose (..))
data Vector
@sjoerdvisscher
sjoerdvisscher / wtf.ts
Created Feb 3, 2021
wtf ala typescript
View wtf.ts
// term variables
let z : int = 123
let y : int = z
// anonymous products & inline types
let k : [ int, int, int ] = [ 1, 2, 3 ]
// sum types and type variables
type Q = A(int) | B(bool)
let qA : Q = A(123)
View FreeCocompl.hs
{-# LANGUAGE RankNTypes, TypeOperators, PolyKinds, FunctionalDependencies, FlexibleInstances, StandaloneKindSignatures, DataKinds #-}
import Prelude hiding (id, (.))
import Control.Category
import Control.Arrow ((+++))
import Data.Kind (Constraint, Type)
type Cat ob = ob -> ob -> Type
type F ob = ob -> Type
-- a presheaf is a functor from C^op to Hask
@sjoerdvisscher
sjoerdvisscher / OpenStarSemiring.lhs
Created Jun 14, 2020
Playing with 'A Very General Method of Computing Shortest Paths'
View OpenStarSemiring.lhs
This is an extension of "A Very General Method of Computing Shortest Paths" to use "open matrices".
This is from a paper "The Open Algebraic Path Problem" by Jade Master https://arxiv.org/abs/2005.06682
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE TypeApplications #-}
> {-# LANGUAGE FlexibleContexts #-}
> {-# LANGUAGE StandaloneDeriving #-}
> {-# LANGUAGE AllowAmbiguousTypes #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> module OpenStarSemiring where