To answer your initial question, you cannot write such an f
from Int
to a type-level inductive representation of integers without a full dependent-type system (which Haskell does not have). However, the problem you describe in the 'context' does not require such a function in Haskell.
I believe the following is roughly what you are looking for:
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, FunctionalDependencies, UndecidableInstances #-}
import Data.HList
data Z = Z
data S n = S n
class Nat t
instance Nat Z
instance Nat n => Nat (S n)
class (Nat n, HList l, HList l') => Shuffle n l l' | n l -> l' where
shuffle :: n -> l -> l'
instance Shuffle Z HNil HNil where
shuffle Z HNil = HNil
instance (HAppend xs (HCons x HNil) ys, HList xs, HList ys) => Shuffle Z (HCons x xs) ys where
shuffle Z (HCons x xs) = hAppend xs (HCons x HNil)
instance (Shuffle n xs ys) => Shuffle (S n) (HCons x xs) (HCons x ys) where
shuffle (S n) (HCons x xs) = HCons x (shuffle n xs)
e.g.
*Main> shuffle (S Z) (HCons 1 (HCons "Hello" (HCons 32 (HCons 500 HNil))))
HCons 1 (HCons 32 (HCons 500 (HCons "Hello" HNil)))
The general technique behind this definition is to first think about how to write the non-dependent-typed version (e.g. here, how to shuffle an element to the end of a list) and to then convert this to the type-level (constraint) version. Note, the recursive structure of shuffle
is exactly mirrored by the recursive structure of constraints in the type class instances.
Does this solve what you are trying to do?