Skip to content

Instantly share code, notes, and snippets.


Nicolas Frisby nfrisby

View GitHub Profile
nfrisby / CovariantN.hs
Created Oct 17, 2012
type class for covariance in any parameter, not just the first (where all parameters are of kind *)
View CovariantN.hs
{-# 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 / Forall.hs
Created Oct 14, 2012
uninstantiable family for safe polykinded universally quantified constraints?
View Forall.hs
{-# 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 / InductiveConstraints.hs
Created Oct 11, 2012
simple demo of "proving" in Haskell via singleton types
View InductiveConstraints.hs
{-# LANGUAGE RankNTypes, TypeFamilies, DataKinds, TypeOperators,
ScopedTypeVariables, PolyKinds, ConstraintKinds, GADTs,
MultiParamTypeClasses, FlexibleInstances, UndecidableInstances,
FlexibleContexts #-}
module InductiveConstraints where
import GHC.Prim (Constraint)
nfrisby / NewGDApp.hs
Created Oct 10, 2012
Representing internal applications of indexed datatypes in generic-deriving
View NewGDApp.hs
{-# 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 / NLong_demo
Created Oct 7, 2012
Demonstration of the usefulness of NLong for type inference
View NLong_demo
-- 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 / GHC_Query
Created Oct 5, 2012
Exploring kind-indexed type constraints in GHC 7.6
View GHC_Query
{-# 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