StringAndIntList

StringAndIntList.hs

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE TypeFamilies      #-}
{-# LANGUAGE TypeOperators     #-}
{-# LANGUAGE PolyKinds         #-}
module StringAndIntList where

data Nat = Z | S Nat

data StringAndIntList (stringCount :: Nat) where
  SINil :: StringAndIntList 'Z
  SCons :: String -> StringAndIntList n -> StringAndIntList ('S n)
  ICons :: Int -> StringAndIntList n -> StringAndIntList n

---------------

type family (x :: Type) `Elem` (xs :: [Type]) :: Bool where
  x `Elem` '[     ]  = 'False
  x `Elem` (x ': xs) = 'True
  x `Elem` (y ': xs) = x `Elem` xs

type family If (p :: Bool) (false :: k) (true :: k) :: k where
  If 'True _ tru = tru
  If 'False fals _ = fals

data StringAndIntList' (stringCount :: Nat) where
  Nil'  :: StringAndIntList' 'Z
  Cons' :: forall x n. (x `Elem` '[ Int , String ]) ~ 'True =>
             x -> StringAndIntList' n -> StringAndIntList' (If (x `Elem` '[ String ]) n ('S n))