Examples for DataKinds and ConstraintKinds

ListApply.hs

{-# 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"