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 B.hs
{-# LANGUAGE BangPatterns #-}
import Data.Time (getCurrentTime, diffUTCTime)
import Control.Parallel.Strategies (parMap, rpar)
import qualified Data.Set as S
import Data.List.Split (chunksOf)
import Data.List (transpose)
cntSeq :: S.Set Int -> [Int] -> Int
cntSeq set xs = foldl (\ c x -> c + (mmbr set x)) 0 xs
@Lysxia
Lysxia / WhytheresnoSTT.hs
Last active Dec 29, 2019
Why there is no ST monad transformer
View WhytheresnoSTT.hs
{-# LANGUAGE RankNTypes #-}
import Control.Monad
import Data.Void
import GHC.Exts (Any)
import Unsafe.Coerce
-- Candidate for "ST monad transformer"
newtype STT s m a = STT ([Any] -> m (a, [Any]))
View RunStateFree.hs
{-# LANGUAGE BangPatterns, RankNTypes, DeriveFunctor #-}
import Control.Monad.Trans.Free (FreeT(..), FreeF(..), foldFreeT)
import Control.Monad.Trans.Free.Church
import Control.Monad.State
import Control.Applicative
import Data.Functor.Identity
import Test.QuickCheck
@Lysxia
Lysxia / PredMonadTrans.v
Created Nov 25, 2019
The predicate monad transformer (PredT M A = (M A -> Prop))
View PredMonadTrans.v
Set Universe Polymorphism.
From Coq Require Import Setoid Morphisms.
From ExtLib Require Import Structures.Monad.
From ITree Require Import ITree.
Variant Cont (R A : Type) : Type :=
| MkCont (runCont : (A -> R) -> R)
View ContPropMonadTrans.v
Set Universe Polymorphism.
From Coq Require Import Setoid Morphisms.
From ExtLib Require Import Structures.Monad.
From ITree Require Import ITree.
Variant Cont (R A : Type) : Type :=
| MkCont (runCont : (A -> R) -> R)
@Lysxia
Lysxia / Rw.v
Created Nov 7, 2019
Trivial example of rewrite with non-transitive relation
View Rw.v
From Coq Require Import Setoid Morphisms.
Inductive Trivial (n : nat) : Prop := T.
Definition neq : nat -> nat -> Prop :=
fun n m => n <> m.
Lemma neq_0_1 : neq 0 1.
Proof.
discriminate.
View A.hs
data Robot = Robot Bearing Coordinates deriving (Eq, Show)
data Bearing = North | South | East | West deriving (Eq, Show)
left :: Bearing -> Bearing
left North = West
left West = South
left South = East
left East = North
View dependenttypesftw.v
Definition nat_eqb (x y : nat) : {x = y} + {x <> y}.
Proof. decide equality. Defined.
Definition choose (x y : nat) :=
if nat_eqb x y then 1
else 2.
Definition lem {x y : nat} (P : x = y -> False) : choose x y = 2 :=
match nat_eqb x y as e return (if e then _ else _) = _ with
| left r => match P r with end
@Lysxia
Lysxia / cont.v
Last active Oct 28, 2019
Half-verify alternative version of monad laws
View cont.v
Parameter m : Type -> Type.
Notation c r a := ((a -> m r) -> m r).
Parameter lift : forall r a, m a -> c r a.
Arguments lift {r a}.
Parameter pure : forall a, a -> m a.
Arguments pure {a}.
Definition unlift {a} : c a a -> m a := fun u => u pure.
View Func.hs
data FuncResult = Ok Integer | NameErr | ArityErr Integer
resultOf :: String -> [Integer] -> FuncResult
resultOf = applyFuncs
[ Func ["D", "derangement", "derangements"] (Arity1 (\n -> derangementR !! fromInteger n))
, Func ["!", "factorial"] (Arity1 factorial)
, Func ["g", "gcd", "euclidean"] (Arity2 gcd)
, Func ["p", "P", "partition"] (Arity2 partition)
, Func ["s", "S", "sterling"] (Arity2 sterling)
, Func ["c", "C", "ncr", "combinations"] (Arity2 ncr)
You can’t perform that action at this time.