Skip to content

Instantly share code, notes, and snippets.

View masaeedu's full-sized avatar

Asad Saeeduddin masaeedu

  • Montreal, QC, Canada
View GitHub Profile
module naryapplicative where
open import Agda.Primitive
module Functor
where
record functor { ℓ } (f : Set Set ℓ) : Set (lsuc ℓ)
where
field
@masaeedu
masaeedu / gist:9c25b89594a2417f6668d2dd00fbcbba
Created March 10, 2020 05:02
Applicative right unit via natural isomorphism
zipr = tabulate . zipf . bimap index index
huskr = tabulate . huskf
Right unit law
---
map2 huskr > zipr > map runit_fwd
= {definitions}
map2 (tabulate < huskf) > (tabulate < zipf < bimap index index) > map runit_fwd
{-# LANGUAGE LambdaCase, DeriveGeneric #-}
module Examples.Biparsing.JSON where
import MyPrelude hiding (exponent)
import GHC.Generics
import GHC.Natural
import Data.List.NonEmpty (NonEmpty(..))
@masaeedu
masaeedu / SOP.Products.hs
Last active March 2, 2020 02:07
Generic (co)products
{-# LANGUAGE LambdaCase, EmptyCase, AllowAmbiguousTypes #-}
module SOP.Products where
import MyPrelude
import GHC.Generics
import Data.Void
import Data.Proxy
@masaeedu
masaeedu / ct.agda
Last active February 15, 2020 21:54
module ct.ct where
open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
record relation (a : Set) (b : Set) : Set₁ where
infix 4 _~_
field
_~_ : a b Set
Resolving dependencies...
Build profile: -w ghc-8.6.4 -O1
In order, the following will be built (use -v for more details):
- adtcorerep-0.0.0 (lib) (first run)
Configuring library for adtcorerep-0.0.0..
Preprocessing library for adtcorerep-0.0.0..
Building library for adtcorerep-0.0.0..
[1 of 3] Compiling Foo ( src/Foo.hs, /mnt/data/depot/git/haskell/experiments/adtcorerep/dist-newstyle/build/x86_64-linux/ghc-8.6.4/adtcorerep-0.0.0/build/Foo.o )
==================== Tidy Core ====================
@masaeedu
masaeedu / Data.Record.Operations.purs
Created October 28, 2019 03:16
Record smooshing
module Data.Record.Operations where
import Prelude
import Data.Functor.Variant (SProxy(..))
import Data.Variant.Internal (RLProxy(..))
import Prim.RowList (Cons, Nil, kind RowList)
import Type.Data.Boolean (True, False, kind Boolean)
import Type.Data.Symbol (class Equals)
import Type.Prelude (class ListToRow, class RowToList)
@masaeedu
masaeedu / FinitaryContainers.hs
Created October 17, 2019 21:44
Finitary containers
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# LANGUAGE AllowAmbiguousTypes, FunctionalDependencies #-}
module FinitaryContainers where
import Data.Proxy
import Data.Functor.Const
import Data.Functor.Identity
import Data.Profunctor
module Adjunctions where
data Coproduct n x
where
First :: x -> Coproduct 'Z x
Next :: Either (Coproduct n x) x -> Coproduct ('S n) x
fold :: Coproduct n x -> x
fold (First x) = x
fold (Next (Right x)) = x
{-# LANGUAGE DataKinds, GADTs, RankNTypes, TypeOperators #-}
module Traversals where
import Control.Monad.Free
type (~>) f g = forall x. f x -> g x
data Nat = Z | S Nat