Skip to content

Instantly share code, notes, and snippets.

View AddrSing.hs
{-# LANGUAGE TemplateHaskell, GADTs, ScopedTypeVariables, PolyKinds, DataKinds,
TypeFamilies, TypeOperators, UndecidableInstances, InstanceSigs,
TypeApplications, FlexibleInstances, StandaloneDeriving #-}
module AddrSing where
import GHC.TypeLits
import Data.Kind
import Data.Singletons.TH
import Data.Singletons.Sigma
@int-index
int-index / Implicit.hs
Last active Apr 10, 2019 — forked from greatBigDot/Implicit.hs
A fixed attempt to represent implicit proof terms in quasi-dependent Haskell.
View Implicit.hs
{-# LANGUAGE LambdaCase, EmptyCase
, EmptyDataDecls, TypeOperators, LiberalTypeSynonyms,
ExistentialQuantification, GADTSyntax, GADTs
, StandaloneDeriving
, InstanceSigs, FlexibleContexts, MultiParamTypeClasses,
FlexibleInstances , TypeSynonymInstances , FunctionalDependencies
, TypeFamilies, TypeFamilyDependencies, DataKinds, PolyKinds,
View gist:ebbbc5b124470787694177b81b8652f1
Prelude Language.Haskell.TH GHC.TypeLits> a <- runQ [t| 1 + 2 |]
Prelude Language.Haskell.TH GHC.TypeLits> a
AppT (AppT (ConT GHC.TypeNats.+) (LitT (NumTyLit 1))) (LitT (NumTyLit 2))
Prelude Language.Haskell.TH GHC.TypeLits> b <- runQ [e| 1 + 2 |]
Prelude Language.Haskell.TH GHC.TypeLits> b
InfixE (Just (LitE (IntegerL 1))) (VarE GHC.Num.+) (Just (LitE (IntegerL 2)))
View NamedDefaults.hs
{-# LANGUAGE KindSignatures, DataKinds, FlexibleInstances, FlexibleContexts,
FunctionalDependencies, TypeFamilies, TypeOperators,
PatternSynonyms, UndecidableInstances, ConstraintKinds,
TypeApplications, ScopedTypeVariables, CPP #-}
module NamedDefaults (FillDefaults, fillDefaults, (!.)) where
import Prelude (Maybe(..), id)
import Data.Kind (Type)
@int-index
int-index / Elem.hs
Created Feb 12, 2018
Type families case split, confluent
View Elem.hs
{-# LANGUAGE RankNTypes, TypeApplications, TypeInType, TypeOperators,
ScopedTypeVariables, TypeFamilies, UndecidableInstances,
GADTs, ConstraintKinds, AllowAmbiguousTypes #-}
module Elem where
import Data.Type.Equality
import Data.Kind
import Unsafe.Coerce
@int-index
int-index / nolog.hs
Last active Dec 14, 2017
Logging not disabled
View nolog.hs
{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, OverloadedStrings, UndecidableInstances #-}
import Control.Monad.Logger
import Control.Monad.Trans
import Control.Monad.Trans.Identity
import Data.Coerce
class Monad m => MonadFoo m where
foo :: m ()
View bistrength.hs
class Bistrength g where
bistrength :: Bifunctor f => g (f a b) -> f (g a) (g b)
instance Bistrength ((,) x) where
bistrength (x, f) = bimap (x,) (x,) f
instance Bistrength ((,,) x y) where
bistrength (x, y, f) = bimap (x,y,) (x,y,) f
View keybase.md

Keybase proof

I hereby claim:

  • I am int-index on github.
  • I am int_index (https://keybase.io/int_index) on keybase.
  • I have a public key ASDdpc-5-1Z79PVP06_HBtD5DQ-q0TkrX3nyQs7cIvSEFQo

To claim this, I am signing this object:

View coherent.hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables, FlexibleContexts #-}
import Control.Monad.Reader
import Data.Reflection
import Data.Tagged
import Data.Proxy
f :: Reader String Int
f = do
a <- ask
@int-index
int-index / polyconstraints-exercise.hs
Last active May 31, 2017
Polyconstraints Exercise: @int-index solution
View polyconstraints-exercise.hs
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
TypeOperators, UndecidableInstances #-}
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds #-}
import Data.Constraint
import Data.Constraint.Forall
class C1 a b
class C2 a b
instance C1 a b => C2 a b