Exploring variadic functions in Haskell

Main.hs

-- See: http://reasonableapproximation.net/2022/04/02/variadic-hm.html

{-# LANGUAGE AllowAmbiguousTypes
           , ConstraintKinds
           , DataKinds
           , FlexibleInstances
           , FunctionalDependencies
           , KindSignatures
           , PolyKinds
           , ScopedTypeVariables
           , TypeApplications
           , TypeFamilies
           , UndecidableInstances
#-}

module Main where

import Data.Type.Nat (Nat(Z, S), Nat1, Nat2, Nat3)
import qualified Data.List as List

------

-- This one comes via
-- McBride, Faking It: Simulating Dependent Types in Haskell
-- (2002, doi: 10.1017/S0956796802004355).

class ZipWith (n :: Nat) fst rest | n fst -> rest where
  manyApp :: [fst] -> rest

instance ZipWith Z t [t] where
  manyApp fs = fs

instance ZipWith n fst rest => ZipWith (S n) (t -> fst) ([t] -> rest) where
  manyApp fs ss = manyApp @n (zipWith ($) fs ss)

nZipWith :: forall n fst rest . ZipWith n fst rest => fst -> rest
nZipWith f = manyApp @n (repeat f)

------

class ListType a t | t -> a where
  list_ :: [a] -> t

-- Pretty sure we could use DList to build this instead of something O(n^2)
instance ListType a [a] where
  list_ = reverse

instance ListType a t => ListType a (a -> t) where
  list_ args = \a -> list_ (a : args)

list :: ListType a t => t
list = list_ []

------

-- This seems to mostly work, but has awful type inference.

type family ListType_' t where
  ListType_' ([a] -> [a]) = a
  ListType_' (a -> t) = a

class ListType' t where
  list_' :: [ListType_' t] -> t

instance {-# OVERLAPPING #-} ListType' ([a] -> [a]) where
  list_' = (++)

instance (ListType' t, ListType_' t ~ a, ListType_' (a -> t) ~ a)
      => ListType' (a -> t) where
  list_' args = \a -> list_' (a : args)

list' :: ListType' t => t
list' = list_' []

------

-- Like with list', awful type inference.

class NZip f t where
  nZip :: [t] -> f

instance NZip [a] a where
  nZip = id

instance NZip f (a, t) => NZip ([t] -> f) a where
  nZip units = \xs -> nZip (zip units xs)

------

class NUnzip n i o | n i -> o where
  nUnzip :: [i] -> o

instance NUnzip Nat1 a [a] where
  nUnzip = id

-- We can't have instances for both (S Z) and (S n), so we have (S Z) and
-- (S (S n)).
instance NUnzip (S n) i o => NUnzip (S (S n)) (i, a) (o, [a]) where
  nUnzip i = let (i_, a) = unzip i in (nUnzip @(S n) i_, a)

------

-- This approach works as long as the initial arguments all have different
-- types. The sortBy instance has bad type inference.

class Sort a b c | a -> b c where
  sort' :: c => a -> b

instance Sort [a] [a] (Ord a) where
  sort' = List.sort

instance Sort (a -> a -> Ordering) ([a] -> [a]) () where
  sort' = List.sortBy

------

main :: IO ()
main = do
  print $ nZipWith @Nat2 ((+) @Int) [1,2,3,4] [5,6,7]

  print (list :: [Int]) -- `list @Int` would be nice, but doesn't work
  print $ 3 : list 4 5 6
  print $ length @[] $ list 4 5 6

  print (list' [3::Int] :: [Int])
  print (list' 2 [3::Int, 4] :: [Int])
  print $ 'a' : list' 'b' "cde"
  print $ (1::Int) : list' 2 [3::Int, 4]

  print (nZip [()] :: [()])
  print (nZip "abc" [1::Int, 2, 3] :: [(Char, Int)])
  print (nZip "abc" "def" [1::Int,2,3,4] :: [((Char, Char), Int)])
  print $ (('x', 'y'), 5)
        : (nZip "abc" "def" [1::Int,2,3,4] :: [((Char, Char), Int)])

  print $ nUnzip @Nat2 [((1, 2), 3), ((4, 5), 6)]
  print $ nUnzip @Nat3 [((1, 2), 3), ((4, 5), 6)]

  print $ sort' [5, 3, 4]
  print $ sort' (\a b -> compare (length @[] @Char a) (length @[] @Char b))
                ["abc", "d", "ef"]