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.

I think that this will not work, as it seems to me to need proper dependent types, which iirc Haskell does not have. The specific part that is the issue is that the type of shuffle would change depending on what the first parameter is, even though this first parameter would have the same type in any case. — user1020786
The usual approach is to use a CPS transform, so you end up with f :: Int -> (forall k. (Countable k) => k -> r) -> r. This works for some use cases, but can get complex. There may also be an approach using the reflection package but I haven't used that myself. A perhaps less-well-founded approach involves abusing template haskell. — John L
It's impossible to go from an Int value to a type, because values are purely runtime and types need to be known at compile time. — shang
@JohnL I was thinking about template haskell but TH is only compile-time, this needs to be runtime. I'll look into the CPS transformation. — rtpg

dorchard dorchard · Accepted Answer · 2013-01-30T10:08:39

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?

haskell - How can I go from values to types?

1 Answers