Iterate a function with different input and output types

Question

I have two functions that rotate a heterogeneous list to the right/left:

hRotateRight :: (HInit xs, HLast xs) => HList xs -> HList (HLastR xs ': HInitR xs)
hRotateRight xs = hLast xs `HCons` hInit xs

hRotateLeft :: HSnoc xs x => HList (x ': xs) -> HList (HSnocR xs x)
hRotateLeft (x `HCons` xs) = hSnoc xs x

Obviously, both functions have different input and output types (except when the input is a singleton). However, they do have the property that any output of the function can also be an input, that is, the function can be iterated.

I'm looking for a type-safe way to do that in Haskell (I'm not sure if that's even possible). Thanks!

Li-yao Xia · Accepted Answer · 2020-05-27 20:26:00Z

That's possible, with the usual caveat that dependently-typed programming in Haskell it full of holes once you start getting into it.

To iterate a function a number of times, we first need a notion of numbers. The simplest representation is Peano naturals, with an associated singleton type, which provides term-level values that are linked to type-level Nats, a link which you wouldn't get with only term-level Nat.

data Nat = Z | S Nat
data SNat n where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

Define iterated rotation at the type level.

-- Note: some renaming happened, dropping type classes and reusing the simpler names for type families.

type Rotate1 xs = HLast xs ': HInit xs

type family RotateN n xs where
  RotateN 'Z xs = xs
  RotateN ('S n) xs = RotateN n (Rotate1 xs)

Using that, define iterated rotation at the term level, making sure to follow the same "structure" as the type-level definition.

hRotateN :: SNat n -> HList xs -> HList (RotateN n xs)
hRotateN SZ xs = xs
hRotateN (SS n) xs = hRotateN n (hRotateRight xs)

Full gist: https://gist.github.com/Lysxia/fabbf6636f212577e89d507b5380f54d

See also Introduction to Singletons, a blog post series by Justin Le.

Collectives™ on Stack Overflow

Iterate a function with different input and output types

1 Answer 1

Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

Comments

Your Answer

Sign up or log in

Post as a guest

Related