haskell - How can I go from values to types?

Question

Imagine I have the following data types and type classes (with proper language extensions):

data Zero=Zero
data Succ n = Succ n
class Countable t where
      count :: t -> Int
instance Countable Zero where
      count Zero = 0

instance (Countable n) => Countable (Succ n) where
      count (Succ n) = 1 + count n

Would it be possible to write a function that gives me , from an Integer, an instance of the proper typeclass instance? Basically, a function f so that count (f n) = n

My attempts have been variants of the following, this gives me some type errors at compile time though:

f::(Countable k)=> Int -> k
f 0 = Zero
f n = Succ $ f (n-1)

I've run into discussions on dependent types a lot while looking for a solution, but I have yet to be able to map those discussions to my use-case.

---

Context: Because I realise that this will get a lot of "why would you want to do this" type of questions...

I'm currently using the Data.HList package to work with heterogeneous lists. In this library, I would like to build a function shuffle which , when given an integer n, would shift the nth element of the list to the end.

For example, if I had l=1:"Hello":32:500 , I'd want shuffle 1 l to give 1:32:500:"Hello".

I've been able to write the specialised function shuffle0 that would answer the usecase for shuffle 0:

shuffle0 ::(HAppend rest (HCons fst HNil) l')=>HCons fst rest -> l'
shuffle0 (HCons fst rest) = hAppend rest (HCons fst HNil)

I've also written this function next that would "wrap" a function , such that next (shuffle n) = shuffle (n+1):

next :: (forall l l'. l -> l') -> (forall e l l'.(HCons e l) -> (HCons e l'))
next f = \(HCons e l)-> HCons e  $ (f l) 

I feel like my type signature might not help, namely there isn't length encoding (which is where problems could appear):

shuffle 0=shuffle0
shuffle n= next (shuffle (n-1))

GHC complains about not being able to deduce the type of shuffle.

This doesn't really surprise me as the type is probably not very well founded.

Intuitively I feel like there should be a mention of the length of the lists. I can get the length of a specific HList type through the HLength type function, and with some nicely chosen constraints rewrite shuffle so that it's sound (at least I think).

The problem is that I still need to get the type-level version of my chosen length, so that I can use it in my call. I'm not even sure if with that this can work but I feel I'll have a better chance.

Answer 1

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?