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
@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)
@Lysxia
Lysxia / IFIF.hs
Last active Oct 5, 2019
Initial/final encodings of initial/final (co)algebras
View IFIF.hs
{- Initial/final encodings of initial/final (co)algebras -}
{-# LANGUAGE GADTs, KindSignatures, RankNTypes #-}
module IFIF where
import Data.Kind (Type)
-- Initial encoding of the initial algebra of f
@Lysxia
Lysxia / HTree.v
Created Oct 3, 2019
Indexed containers for game semantics
View HTree.v
(** An (indexed) "container" encodes an indexed recursive type. *)
(** A container can also be seen as a game, with
- [ix] as the type of positions,
- [shape i] the Player moves at position [i],
- [pos i s] the Opponent moves after Player plays move [s] on position [i],
- [posix i s p] the new position after moves [s] and [p] from position [i].
*)
Module Export Container.
Record container :=
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
You can’t perform that action at this time.