Skip to content

Instantly share code, notes, and snippets.

Asad Saeeduddin masaeedu

Block or report user

Report or block masaeedu

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@masaeedu
masaeedu / gist:9c25b89594a2417f6668d2dd00fbcbba
Created Mar 10, 2020
Applicative right unit via natural isomorphism
View gist:9c25b89594a2417f6668d2dd00fbcbba
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
View Examples.Biparsing.JSON.hs
{-# 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 Mar 2, 2020
Generic (co)products
View SOP.Products.hs
{-# LANGUAGE LambdaCase, EmptyCase, AllowAmbiguousTypes #-}
module SOP.Products where
import MyPrelude
import GHC.Generics
import Data.Void
import Data.Proxy
View ct.agda
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
View out.txt
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 ====================
View Data.Record.Operations.purs
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)
View FinitaryContainers.hs
{-# 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
View CoAndProductAdjunction.hs
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
View gist:a2e58e1aa350d139ea97a03fbb3fdbda
{-# 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
View ProfunctorOpticsButWithMonads.hs
{-# LANGUAGE RankNTypes, TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeApplications, DuplicateRecordFields, FlexibleContexts, ScopedTypeVariables #-}
module Main where
import Data.IORef
import Control.Monad.Reader
import Control.Monad.State
type (~>) f g = forall x. f x -> g x
newtype Product f g a = Product { runProduct :: (f a, g a) }
You can’t perform that action at this time.