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 a.hs
{-# LANGUAGE RankNTypes, DerivingStrategies, GeneralizedNewtypeDeriving #-}
-- Defaults to newtype
newtype T_Def = T_Def Bool
deriving (Eq, Ord, Bounded)
-- Stock
newtype T_S = T_S Bool
deriving stock (Eq, Ord, Bounded)
View viacodensity.hs
{-# Language KindSignatures, RankNTypes, DerivingVia #-}
newtype Foo i o m r = Foo (Await i m r -> Yield o m r -> m r)
newtype Pipe i o m a = Pipe (forall xx. (a -> Await i m xx -> Yield o m xx -> m xx) -> (Await i m xx -> Yield o m xx -> m xx))
deriving (Functor, Applicative, Monad)
via Codensity (Foo i o m)
-- Fluff --
View GHas.hs
data Path = L Path | R Path | Here
data MPath = NotFound | Conflict | Found Path
type family Search a (f :: k -> Type) :: MPath where
-- ...
Search a (f :*: g) = OrPath (Search a f) (Search a g)
Search a (K1 i c) = Check a c
type family Check a c where
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
You can’t perform that action at this time.