Skip to content

Instantly share code, notes, and snippets.

@RyanGlScott
RyanGlScott / Foo.hs
Last active Jan 9, 2019
Can you implement `foo` without `coerce`?
View Foo.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Coerce
type family F a
newtype T1 = MkT1 (forall a. F a)
newtype T2 = MkT2 (forall a. F a)
@RyanGlScott
RyanGlScott / SubstRep1.hs
Last active Dec 11, 2018
How to derive a Generic instance using nothing but Generic1
View SubstRep1.hs
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module SubstRep1 where
@RyanGlScott
RyanGlScott / CTuples.hs
Last active May 16, 2019
Partially applicable constraint tuple type constructors
View CTuples.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710
{-# LANGUAGE NullaryTypeClasses #-}
#endif
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses #-}
@RyanGlScott
RyanGlScott / S.hs
Last active Nov 30, 2018
Conor McBride's S combinator in GHC
View S.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module S where
import Data.Kind
@RyanGlScott
RyanGlScott / ElimNat.hs
Last active Nov 14, 2018
Type-level eliminators in GHC!
View ElimNat.hs
#!/usr/bin/env cabal
{- cabal:
build-depends: base >= 4.12
, singleton-nats >= 0.4.1
, singletons >= 2.5.1
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
@RyanGlScott
RyanGlScott / Foo.idr
Created Nov 7, 2018
Why doesn't this typecheck?
View Foo.idr
module Foo
%default total
interface C a where
T' : Type
T : (a : Type) -> C a => Type
T a = T' {a}
interface (C a, Show (T a)) => D a where
@RyanGlScott
RyanGlScott / KindOf.md
Last active Mar 20, 2019
KindOf is a crazy, crazy type.
View KindOf.md

I've discovered something how to do something that GHC never intended you to be able to do, and I'm wondering if there's a way to abuse this to do interesting things.

It's known that you can express visible, dependent quantification at the kind level:

data A a :: a -> Type
λ> :kind A
@RyanGlScott
RyanGlScott / PartitionNS.hs
Last active Nov 27, 2018
Generalized partitionEithers
View PartitionNS.hs
#!/usr/bin/env cabal
{- cabal:
build-depends: base >= 4.9
, QuickCheck >= 2.12
, sop-core >= 0.4
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
@RyanGlScott
RyanGlScott / IdleThoughtsOnGADTsAsNewtypes.hs
Last active Sep 15, 2018
How some GADTs (might) be represented as newtypes
View IdleThoughtsOnGADTsAsNewtypes.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module IdleThoughtsOnGADTsAsNewtypes where
@RyanGlScott
RyanGlScott / SGenericSingKind.hs
Last active Jul 10, 2018
A generic implementation of SingKind
View SGenericSingKind.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}