Skip to content

Instantly share code, notes, and snippets.

View gergoerdi's full-sized avatar

Gergő Érdi gergoerdi

View GitHub Profile
@gergoerdi
gergoerdi / Setup.hs
Last active March 15, 2021 11:33
JustBeforeBuildingCabal
import Distribution.Simple
import Distribution.Simple.BuildTarget
import Distribution.Simple.LocalBuildInfo
import Distribution.Simple.Setup
import Distribution.Types.ComponentRequestedSpec
import Distribution.Types.Lens
import Data.List (sort, nub)
import Control.Monad (when, forM_)
import System.Directory
liftTypeRep :: TypeRep a -> TH.Type
liftTypeRep ty = L.foldl AppT t0 [liftTypeRep ty' | SomeTypeRep ty' <- args]
where
(con, args) = splitApps ty
t0 = ConT $ mkName (tyConModule con <> "." <> tyConName con)
traverseTerm : (Applicative f) => (Var vars1 -> f (Term vars2)) -> (Term vars1 -> f (Term vars2))
traverseTerm go (Local idx p) = go (MkVar p)
traverseTerm go (Ref nt x) = pure $ Ref nt x
traverseTerm go (Meta x ts) = Meta x <$> traverse (traverseTerm go) ts
traverseTerm go (Bind x b scope) = Bind x <$> traverse (traverseTerm go) b <*> traverseTerm go' scope
where
go' : Var (x :: vars1) -> f (Term (x :: vars2))
go' (MkVar First) = pure $ Local _ First
go' (MkVar (Later p)) = weaken <$> go (MkVar p)
traverseTerm go (App f e) = App <$> traverseTerm go f <*> traverseTerm go e
function r(e) {
var n =
[[1.11e11, 0.6819],
[8.12e10, 0.6518],
@gergoerdi
gergoerdi / CatMonad.hs
Created July 16, 2019 14:53
Category-indexed monads, now with more type inference!
-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/7331df3abee0aceacd3d9a74b567f54c
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs, TypeOperators #-}
{-# LANGUAGE TypeApplications, RebindableSyntax #-}
import Prelude hiding (id, (.))
import Control.Category
@gergoerdi
gergoerdi / CatMonad.hs
Last active July 16, 2019 14:32
Category-indexed monads
-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE GADTs, TypeOperators #-}
{-# LANGUAGE TypeApplications, RebindableSyntax, RecordWildCards #-}
import Prelude hiding (id, (.))
import Control.Category
import Data.Kind
@gergoerdi
gergoerdi / CatMonadCounter.hs
Last active July 16, 2019 14:07
Nat as a type-level category, to be used as the index of a category-indexed monad
-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE TypeApplications, TypeOperators, GADTs #-}
import Prelude hiding (id, (.))
import Control.Category
import Data.Kind
import GHC.TypeLits
@gergoerdi
gergoerdi / Int.agda
Created November 11, 2018 13:52
Int as a HIT
{-# OPTIONS --cubical #-}
module Int where
open import Data.Nat renaming (_+_ to _+̂_)
open import Cubical.Core.Prelude
open import Utils
Same : ℕ → ℕ → ℕ → ℕ → Set
Same x y x′ y′ = x +̂ y′ ≡ x′ +̂ y
@gergoerdi
gergoerdi / Quotient.agda
Created November 11, 2018 07:59
Cubical quotient types
{-# OPTIONS --cubical #-}
module Quotient where
open import Cubical.Core.Prelude
Reflexive : ∀ {ℓ} {A : Set ℓ} → (A → A → Set ℓ) → Set _
Reflexive _∼_ = ∀ x → x ∼ x
module Quot {ℓ} (A : Set ℓ) (_∼_ : A → A → Set ℓ) (∼-refl : Reflexive _∼_) where
data Q : Set ℓ where
open import Agda.Builtin.FromNat
open import Data.Fin
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Nat renaming (_≤?_ to _N≤?_)
open import Data.Unit
instance
NumFin : ∀ {n} → Number (Fin n)