Skip to content

Instantly share code, notes, and snippets.

@konn
Created Jun 6, 2012
Embed
What would you like to do?
Examples for DataKinds and ConstraintKinds
{-# LANGUAGE GADTs, TypeFamilies, DataKinds, ConstraintKinds #-}
{-# LANGUAGE TypeOperators, ScopedTypeVariables #-}
module Main where
import GHC.Exts (Constraint)
import Control.Applicative
data NAry (as :: [*]) a where
Value :: a -> NAry '[] a
Arg :: (b -> NAry xs a) -> NAry (b ': xs) a
instance Show a => Show (NAry xs a) where
showsPrec d (Value a) = showParen (d > 10) $ showString "Value " . showsPrec d a
showsPrec d (Arg f) = showParen (d > 10) $ showString "#Argument#"
data NAry' (as :: [*]) a = (as ~ '[]) => Value' a
| forall b xs . (as ~ (b ': xs))
=> Arg' (b -> NAry' xs a)
type family (xs :: [*]) :~> a :: *
type instance '[] :~> a = a
type instance (x ': xs) :~> a = x -> xs :~> a
infixr :~>
fromNAry :: NAry xs a -> xs :~> a
fromNAry (Value a) = a
fromNAry (Arg f) = fromNAry . f
data SList (as :: [*]) where
SNil :: SList '[]
SCons :: a -> SList xs -> SList (a ': xs)
class SingList k where
slist :: SList k
instance SingList '[] where
slist = SNil
instance SingList xs => SingList (x ': xs) where
slist = SCons undefined slist
toNAry' :: SList xs -> (xs :~> a) -> NAry xs a
toNAry' SNil a = Value a
toNAry' (SCons _ ts) f = Arg $ toNAry' ts . f
toNAry :: forall xs a. SingList xs => (xs :~> a) -> NAry xs a
toNAry = toNAry' (slist :: SList xs)
type family All (cxt :: * -> Constraint) (xs :: [*]) :: Constraint
type instance All cxt '[] = ()
type instance All cxt (x ': xs) = (cxt x, All cxt xs)
type Readable as = All Read as
applyReadList :: Readable as => NAry as a -> [String] -> Maybe a
applyReadList (Value a) [] = Just a
applyReadList (Arg f) (x:xs) = applyReadList (f $ read x) xs
applyReadList _ _ = Nothing
applyHomoList :: All ((~) b) as => NAry as a -> [b] -> Maybe a
applyHomoList (Value a) [] = Just a
applyHomoList (Arg f) (x:xs) = applyHomoList (f x) xs
applyHomoList _ _ = Nothing
type family ZipC (c :: * -> * -> Constraint) (as :: [*]) (bs :: [*]) :: Constraint
type instance ZipC c '[] xs = ()
type instance ZipC c xs '[] = ()
type instance ZipC c (x ': xs) (y ': ys) = (c x y, ZipC c xs ys)
applyHeteroList :: NAry as a -> SList as -> a
applyHeteroList (Value a) SNil = a
applyHeteroList (Value a) (SCons _ _) = a
applyHeteroList (Arg f) (SCons s ts) = applyHeteroList (f s) ts
applyHeteroList (Arg f) SNil = error "This would never happen"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment