Skip to content

Instantly share code, notes, and snippets.

Xia Li-yao Lysxia

Block or report user

Report or block Lysxia

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
View tcase.v
Require Import List Arith Ascii String Fin.
Require Import MetaCoq.Template.All.
Import ListNotations MonadNotation.
Set Universe Polymorphism.
Local Open Scope string_scope.
(* Get the [one_inductive_body] from a [mutual_inductive_body].
Fails if there is more than one. *)
Definition get_ind_body (tyDef : mutual_inductive_body)
View CatMonad.hs
{-# LANGUAGE GADTs, FunctionalDependencies, FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
module CatMonad where
import Control.Category as C
import Data.Kind
class CatMonad (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) | c -> m where
type Id c :: c x x
type Cat c (f :: c x y) (g :: c y z) :: c x z
@Lysxia
Lysxia / CatMonad.hs
Last active Jul 15, 2019
Monads indexed by categories
View CatMonad.hs
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
module CatMonad where
import Control.Category as C
import Data.Kind
class CatMonad (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) where
type Id m :: c x x
type Cat m (f :: c x y) (g :: c y z) :: c x z
View free.v
(* Free applicative functors *)
Implicit Type f : Type -> Type.
Implicit Type a b c : Type.
(* Same as https://hackage.haskell.org/package/free-5.1.1/docs/Control-Applicative-Free.html *)
Inductive Free f a : Type :=
| Pure : a -> Free f a
| Ap {b} : f b -> Free f (b -> a) -> Free f a
.
@Lysxia
Lysxia / komonad.v
Created Jul 4, 2019
Is list a comonad in the Kleisli category of option?
View komonad.v
Require Import List. Import ListNotations.
Require Import FunctionalExtensionality.
Definition kat {a b c} (f : a -> option b) (g : b -> option c) : a -> option c :=
fun x =>
match f x with
| None => None
| Some y => g y
end.
View V.hs
{-# LANGUAGE
TypeFamilies,
ConstraintKinds,
FlexibleInstances,
FlexibleContexts,
MultiParamTypeClasses,
StandaloneDeriving,
UndecidableInstances,
QuantifiedConstraints,
TypeApplications,
View lts-11.22-ghc-8.2.2
json-data/twitter1.json :: 60000 times json-data/twitter1.json :: 60000 times
1.152 seconds, 52086 parses/sec, 42.471 MB/sec 1.152 seconds, 52104 parses/sec, 42.485 MB/sec
json-data/twitter1.json :: 60000 times json-data/twitter1.json :: 60000 times
1.160 seconds, 51706 parses/sec, 42.161 MB/sec 1.149 seconds, 52233 parses/sec, 42.591 MB/sec
json-data/twitter1.json :: 60000 times json-data/twitter1.json :: 60000 times
1.155 seconds, 51930 parses/sec, 42.344 MB/sec 1.150 seconds, 52168 parses/sec, 42.538 MB/sec
0.8 KB: 52086 msg\/sec (42.5 MB\/sec) 0.8 KB: 52234 msg\/sec (42.6 MB\/sec)
json-data/twitter10.json :: 13000 times json-data/twitter10.json :: 13000 times
1.314 seconds, 9890 parses/sec, 62.198 MB/sec 1.299 seconds, 10003 parses/sec, 62.910 MB/sec
json-data/twitter10.json :: 13000 times json-data/twitter10.json :: 13000 times
View lts-11.22-ghc-8.2.2-dupkeys
json-data/twitter1.json :: 60000 times
1.186 seconds, 50572 parses/sec, 41.236 MB/sec
json-data/twitter1.json :: 60000 times
1.185 seconds, 50627 parses/sec, 41.281 MB/sec
json-data/twitter1.json :: 60000 times
1.173 seconds, 51171 parses/sec, 41.725 MB/sec
0.8 KB: 51171 msg\/sec (41.7 MB\/sec)
json-data/twitter10.json :: 13000 times
1.354 seconds, 9598 parses/sec, 60.358 MB/sec
json-data/twitter10.json :: 13000 times
@Lysxia
Lysxia / ArbitraryFix.hs
Last active Jun 19, 2019
Arbitrary for Fix with generic-random and recursion-schemes
View ArbitraryFix.hs
{-# LANGUAGE
DeriveGeneric,
FlexibleContexts,
FlexibleInstances,
TypeFamilies,
RankNTypes #-}
import GHC.Generics
import Generic.Random
import Generic.Data (gliftShowsPrec)
@Lysxia
Lysxia / Free.hs
Created Jun 6, 2019
Playing with higher-order free monads
View Free.hs
{-# LANGUAGE
DeriveFunctor,
DerivingVia,
StandaloneDeriving,
DataKinds,
PolyKinds,
RankNTypes,
InstanceSigs,
GADTs,
TypeFamilies,
You can’t perform that action at this time.