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 retry_futures.rs
/// Retry a function either until it succeeds, or until it fails `1+retries` times.
fn retry_future<F, T>(retries: usize, mut run: F) -> impl Future<Item=T::Item, Error=T::Error>
where F: FnMut() -> T,
T: Future,
{
futures::future::loop_fn(retries, move |retries| {
run().map(|t| { futures::future::Loop::Break(t) }).or_else(move |e| {
futures::future::result(
if retries == 0 { Err(e) }
else { Ok(futures::future::Loop::Continue(retries-1)) })
View P.hs
{-# LANGUAGE RankNTypes, GADTs #-}
data Foo a = B ((a ~ Int) => a)
-- Doesn't check
-- f :: Foo a -> Int
-- f (B n) = n
data Foo' a where
B' :: (a ~ Int) => a -> Foo' a
View HTMLFromLabel.hs
{-# LANGUAGE
AllowAmbiguousTypes,
TypeApplications,
ScopedTypeVariables,
FlexibleInstances,
MultiParamTypeClasses,
TypeFamilies,
OverloadedLabels,
OverloadedStrings #-}
View pacodep.v
Require Import Paco.paco.
Module KO.
Definition test A (r : A -> Prop) : A -> Prop := fun _ => False.
Definition ptest A : A -> Prop := paco1 (test A) bot1.
Goal forall (A : Type) (l : A),
ptest A l.
View GadtReadVariadic.hs
{-# LANGUAGE
-- Unsurprisingly, we're going to talk about GADTs.
GADTs,
-- Type-level functions, data types, and polymorphism
TypeFamilies,
DataKinds,
PolyKinds,
-- Explicit type applications
View MonadIx.hs
{-# LANGUAGE
BlockArguments,
InstanceSigs,
TypeOperators,
DataKinds,
PolyKinds,
RankNTypes,
ScopedTypeVariables,
GADTs
#-}
@Lysxia
Lysxia / GadtRead.hs
Created May 15, 2019
Generic parser for GADTs with kind-generics (composed with an existential type, in the second half)
View GadtRead.hs
{-# LANGUAGE
QuantifiedConstraints,
AllowAmbiguousTypes,
TypeApplications,
ScopedTypeVariables,
RankNTypes,
GADTs,
DataKinds,
PolyKinds,
FlexibleContexts,
@Lysxia
Lysxia / GadtRead.hs
Created May 15, 2019
Generic parser for GADT with kind-generics
View GadtRead.hs
{-# LANGUAGE
AllowAmbiguousTypes,
TypeApplications,
ScopedTypeVariables,
GADTs,
DataKinds,
PolyKinds,
FlexibleContexts,
FlexibleInstances,
MultiParamTypeClasses,
View FieldHandler.hs
{-# LANGUAGE
DataKinds,
PolyKinds,
MultiParamTypeClasses,
TypeOperators,
DeriveGeneric,
KindSignatures,
FlexibleContexts,
FlexibleInstances,
TypeFamilies,
View SM.hs
{-# LANGUAGE
EmptyCase,
DataKinds,
PolyKinds,
KindSignatures,
GADTs,
FlexibleContexts,
FlexibleInstances,
You can’t perform that action at this time.