Skip to content

Instantly share code, notes, and snippets.

View Lysxia's full-sized avatar
🦅
Rocqing

Xia Li-yao Lysxia

🦅
Rocqing
353 followers · 55 following
View GitHub Profile
@Lysxia
Lysxia / FieldNames.hs
Created April 30, 2019 21:28
List of field names for generic record types
{-# LANGUAGE FlexibleContexts, FlexibleInstances, KindSignatures, TypeApplications,
TypeOperators, PolyKinds, ScopedTypeVariables, UndecidableInstances, DeriveGeneric #-}
import GHC.Generics
import Data.Proxy
class GFieldNames (f :: * -> *) where
gFieldNames :: proxy f -> [String]
instance Selector s => GFieldNames (S1 s f) where
@Lysxia
Lysxia / SG.hs
Last active May 3, 2019 12:42
Deriving Semigroup for HKD records
{-# LANGUAGE
AllowAmbiguousTypes,
DeriveGeneric,
FlexibleInstances,
QuantifiedConstraints,
TypeApplications,
UndecidableInstances
#-}
import GHC.Generics
import Control.Applicative
@Lysxia
Lysxia / ZeroLengthVectorIsNil.v
Created May 8, 2019 00:50
Require Import Vector.
Require Import Program.
Definition fff {A} (h : Vector.t A 0) : h = Vector.nil _ :=
match h in Vector.t _ n return match n return Vector.t A n -> Prop with
| O => fun h => h = Vector.nil _
| S _ => fun _ => True
end h
with
| Vector.nil _ => eq_refl
@Lysxia
Lysxia / VariadicArr.hs
Created May 11, 2019 16:04
{-# LANGUAGE
AllowAmbiguousTypes,
FlexibleContexts,
FlexibleInstances,
MultiParamTypeClasses,
UndecidableInstances,
TypeApplications
#-}
import Control.Category hiding ((.), id)
@Lysxia
Lysxia / SM.hs
Last active May 17, 2019 02:40
Type-safe extensible state machine https://stackoverflow.com/questions/50579397/extensible-state-machines-in-haskell/50588021#50588021
{-# LANGUAGE
EmptyCase,
DataKinds,
PolyKinds,
KindSignatures,
GADTs,
FlexibleContexts,
FlexibleInstances,
@Lysxia
Lysxia / FieldHandler.hs
Last active May 13, 2019 16:36
https://www.reddit.com/r/haskell/comments/bo2xdh/how_to_build_record_fields_out_of_sum_type/
{-# LANGUAGE
DataKinds,
PolyKinds,
MultiParamTypeClasses,
TypeOperators,
DeriveGeneric,
KindSignatures,
FlexibleContexts,
FlexibleInstances,
TypeFamilies,
@Lysxia
Lysxia / GadtRead.hs
Created May 15, 2019 22:10
Generic parser for GADT with kind-generics
{-# LANGUAGE
AllowAmbiguousTypes,
TypeApplications,
ScopedTypeVariables,
GADTs,
DataKinds,
PolyKinds,
FlexibleContexts,
FlexibleInstances,
MultiParamTypeClasses,
@Lysxia
Lysxia / GadtRead.hs
Created May 15, 2019 23:06
Generic parser for GADTs with kind-generics (composed with an existential type, in the second half)
{-# LANGUAGE
QuantifiedConstraints,
AllowAmbiguousTypes,
TypeApplications,
ScopedTypeVariables,
RankNTypes,
GADTs,
DataKinds,
PolyKinds,
FlexibleContexts,
@Lysxia
Lysxia / MonadIx.hs
Created May 18, 2019 13:23
MonadIx (example instance of the interface described in https://stackoverflow.com/questions/28690448/what-is-indexed-monad/28696299#28696299)
{-# LANGUAGE
BlockArguments,
InstanceSigs,
TypeOperators,
DataKinds,
PolyKinds,
RankNTypes,
ScopedTypeVariables,
GADTs
#-}
@Lysxia
Lysxia / GadtReadVariadic.hs
Last active May 31, 2020 05:51
{-# LANGUAGE
-- Unsurprisingly, we're going to talk about GADTs.
GADTs,
-- Type-level functions, data types, and polymorphism
TypeFamilies,
DataKinds,
PolyKinds,
-- Explicit type applications