Skip to content

Instantly share code, notes, and snippets.

@nfrisby
nfrisby / CovariantN.hs
Created October 17, 2012 20:52
type class for covariance in any parameter, not just the first (where all parameters are of kind *)
{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
UndecidableInstances, FlexibleContexts #-} -- for the hacky bit
{-# LANGUAGE GADTs #-} -- just for an example
module CovariantN where
import GHC.Prim (Any) -- just for convenience
@nfrisby
nfrisby / Forall.hs
Created October 14, 2012 01:05
uninstantiable family for safe polykinded universally quantified constraints?
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds, Rank2Types,
ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances, UndecidableInstances, MultiParamTypeClasses
#-} -- only for examples
module Proposed.Data.Constraint.Forall
(module Data.Constraint,
Forall, Bottom, inst) where
@nfrisby
nfrisby / InductiveConstraints.hs
Created October 11, 2012 22:09
simple demo of "proving" in Haskell via singleton types
{-# LANGUAGE RankNTypes, TypeFamilies, DataKinds, TypeOperators,
ScopedTypeVariables, PolyKinds, ConstraintKinds, GADTs,
MultiParamTypeClasses, FlexibleInstances, UndecidableInstances,
FlexibleContexts #-}
module InductiveConstraints where
import GHC.Prim (Constraint)
@nfrisby
nfrisby / NewGDApp.hs
Created October 10, 2012 22:02
Representing internal applications of indexed datatypes in generic-deriving
{-# LANGUAGE TypeFamilies, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}
module NewGDApp where
import GHC.Generics hiding ((:.:)) -- I'm proposing an alternative to @:.:@.
-- Only for representations of constructor arguments, ie the leaves of @:*:@.
@nfrisby
nfrisby / NLong_demo
Created October 7, 2012 04:21
Demonstration of the usefulness of NLong for type inference
-- naturals
data Nat = Z | S Nat
-- indexes in the type list
type family Nth (n :: Nat) (ts :: [k]) :: k
type instance Nth Z (a ': as) = a
type instance Nth (S n) (a ': as) = Nth n as
-- represents an uncurried application of t
data family W (t :: k) :: [*] -> *
@nfrisby
nfrisby / GHC_Query
Created October 5, 2012 21:39
Exploring kind-indexed type constraints in GHC 7.6
{-# LANGUAGE PolyKinds, GADTs, DataKinds, TypeFamilies, TypeOperators,
MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
UndecidableInstances #-}
-- this gist demonstrates some GHC 7.6 behaviors that I'm seeing as some type errors (example at the bottom).
module GHC_Query where
data Proxy (t :: k) = Proxy
data KindProxy (t :: *) = KindProxy -- a type-level proxy for kinds