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 GFunctor.hs
class GFunctor (p :: c -> c -> *) (q :: d -> d -> *) (f :: c -> Exp d)
where
gfmap :: p x y -> q (f @@ x) (f @@ y)
instance (GFunctor p q f, GFunctor q r g) => GFunctor p r (g . f) where
gfmap = gfmap @q @r @g . gfmap @p @q @f
data (.) :: (d -> Exp e) -> (c -> Exp d) -> (c -> Exp e)
type instance Eval ((f . g) x) = Eval (f (Eval (g x))
View E.hs
type Lets = Exp -> Exp
-- "Stack of lets", functions of this form:
-- (Let b1 . Let b2 . ... . Let bn)
snoc :: Lets -> (Var, Exp) -> Lets
snoc k b = k . Let b
type M = State (T.Text, Int, Lets)
push :: (Var, Exp) -> M Exp
@Lysxia
Lysxia / HHFree.hs
Last active Sep 16, 2019
doubly-indexed `Free` profunctor, `lmap` using doubly-indexed recursion-schemes
View HHFree.hs
{-# LANGUAGE InstanceSigs, RankNTypes, PolyKinds, DataKinds, TypeOperators, TypeFamilies, FlexibleContexts, BlockArguments, ScopedTypeVariables #-}
module HHFree where
import Data.Profunctor
import Data.Profunctor.Yoneda
import Data.Profunctor.Composition
type (~~>) f g = forall a b. f a b -> g a b
@Lysxia
Lysxia / reverse.v
Created Sep 14, 2019
Reverse lists in linear time with difference lists
View reverse.v
Require Import List.
Import ListNotations.
Fixpoint reverse {A} (xs : list A) : list A :=
match xs with
| [] => []
| x :: xs => reverse xs ++ [x]
end.
Module DList.
View containers.v
Set Implicit Arguments.
Set Contextual Implicit.
Record container : Type := {
shape : Type;
pos : shape -> Type;
}.
Inductive ext (c : container) (a : Type) : Type := {
this_shape : shape c;
View A.v
Goal (0 = 0 /\ 1 = 1).
Proof.
split.
all: reflexivity.
Qed.
Ltac foo := split.
Goal (0 = 0 /\ 1 = 1).
Proof.
View A.hs
{-# LANGUAGE KindSignatures #-}
module A where
class C (f :: * -> * -> *)
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 --
@Lysxia
Lysxia / PseudoLinearTypes.hs
Created Jan 1, 2019
An indexed monad to count mallocs and frees
View PseudoLinearTypes.hs
{-# LANGUAGE
DataKinds,
FlexibleInstances,
FlexibleContexts,
PolyKinds,
ScopedTypeVariables,
TypeApplications,
TypeFamilies,
TypeInType,
TypeOperators #-}
You can’t perform that action at this time.