Constructing function that builds heterogeneous list from all its arguments

Question

Given cons :: x -> f xs -> f (x ': xs) and nil :: f '[]

How can I construct build :: forall xs . ? such that for given xs ~ '[x1, x2 ... xn], build :: x1 -> x2 -> ... -> xn -> f '[x1, x2, ..., xn]

The idea is that I could apply such function in a following manner ($ x) . ($ y) . ($ z) $ build

Answer 1

{-# LANGUAGE TypeFamilies, GADTs, RankNTypes
           , FlexibleInstances, MultiParamTypeClasses
           , FlexibleContexts, UndecidableInstances
           , DataKinds, TypeInType, TypeOperators
           , AllowAmbiguousTypes, TypeApplications
           , ScopedTypeVariables, UnicodeSyntax
           , StandaloneDeriving #-}

import Data.Kind 
import Data.HList

class Buildable (l :: [Type]) (m :: [Type]) where
  type Buildup l m :: Type
  build' :: (HList m -> HList l) -> Buildup l m

instance Buildable l '[] where
  type Buildup l '[] = HList l
  build' prep = prep HNil
instance Buildable l m => Buildable l (x ': m) where
  type Buildup l (x ': m) = x -> Buildup l m
  build' prep x = build' (prep . HCons x)

type Builder l = (Buildable l l) => Buildup l l

build :: ∀ l . Builder l
build = build' @l @l id

Same basic idea as Li-yao Xia, but with type families instead of helper MPTC-arguments. Advantages: clearer what's going on, and it's not necessary to give local signatures to the arguments of build.

*Main> build @('[Int, Bool]) 3 True
H[3,True]

Answer 2

Here's code that works. There's likely too much to explain; feel free to ask questions about this implementation in the comments, and I might extend this answer to answer them.

• To search for more related questions on SO and elsewhere, this falls under the commonly discussed topic of "variadic functions in Haskell", i.e., functions with variable number of arguments.

• A core concept to know about is how the type class instance solver works; the GHC user guide gives a summary.

{-# LANGUAGE
  AllowAmbiguousTypes,
  DataKinds,
  FlexibleInstances,
  MultiParamTypeClasses,
  ScopedTypeVariables,
  TypeOperators,
  TypeFamilies,
  UndecidableInstances,
  TypeApplications #-}


-- Tagless-style heterogeneous lists
class HList f where
  nil :: f '[]
  cons :: x -> f xs -> f (x ': xs)


class HList f => Build_ f xs r b where
  build_ :: (f xs -> r) -> b

instance (HList f, xs ~ '[], f ~ g, r ~ g ys) => Build_ f xs r (g ys) where
  build_ c = c nil

instance (Build_ f xs r b, xxs ~ (x ': xs)) => Build_ f xxs r (x -> b) where
  build_ c x = build_ (\xs -> c (cons x xs))

class    Build_ f xs (f xs) b => Build f xs b
instance Build_ f xs (f xs) b => Build f xs b

build :: forall f xs b. Build f xs b => b
build = build_ @f @xs @(f xs) @b id


example :: HList f => f '[Int, Bool]
example = build (3 :: Int) True

---

Could you explain why ~ equalities are required here and cannot be simplified by directly substituting one type with the other?

This is sometimes called "the constraint trick".

The main idea is that, to decide which instance to pick, the constraint solver only looks to the right of =>, the instance head.

In the second instance's head above, if you put (x ': xs) instead of a variable xxs, so the head becomes Build_ f (x ': xs) r (x -> b), then that instance will be picked only when you already know that the list begins with a cons (':). However, that list is initially unknown (unless the user annotates build with the list explicitly), so that instance would not be picked. By making the instance Build_ f xxs r (x -> b), that allows the instance to be picked based only on the arguments of build_ (based on the fact that it has at least one more). After the instance is picked, the constraints on the left of => are generated, allowing the body of the instance to type check and the instance solver to make more progress.

The equality constraints on the other instances are there for similar reasons. They are constraints you need to make the body of the instance typecheck, but it is not knowledge the constraint solver has a priori when trying to solve a Build_ constraint.