Lift.hs

-- Inspired by https://github.com/goldfirere/video-resources/blob/main/2021-07-06-zipWith/ZipWith.hs

{-# LANGUAGE StandaloneKindSignatures, DataKinds, TypeOperators,
             TypeFamilies, UndecidableInstances, GADTs, ScopedTypeVariables,
             TypeApplications, FlexibleInstances, FlexibleContexts,
             ConstraintKinds, FunctionalDependencies, AllowAmbiguousTypes #-}

module Lift where

import Data.Kind
import Data.Proxy

type LiftsFrom :: (Type -> Type) -> Type -> Type
type family LiftsFrom f t where
  LiftsFrom f (arg -> res) = f arg -> LiftsFrom f res
  LiftsFrom f other        = f other

type LiftsFromWitness :: (Type -> Type) -> Type -> Type
data LiftsFromWitness f t where
  LiftsFromFun :: LiftsFromClass f res => LiftsFromWitness f (arg -> res)
  LiftsFromNil :: LiftsFrom f other ~ f other => LiftsFromWitness f other

type LiftsFromClass :: (Type -> Type) -> Type -> Constraint
class LiftsFromClass f t where
  witness :: LiftsFromWitness f t

instance {-# OVERLAPPING #-} (LiftsFromClass f res) => LiftsFromClass f (arg -> res) where
  witness = LiftsFromFun

instance {-# OVERLAPPABLE #-} LiftsFrom f other ~ f other => LiftsFromClass f other where
  witness = LiftsFromNil

lift :: forall t f. (Applicative f, LiftsFromClass f t) => t -> LiftsFrom f t
lift fun = go (pure fun)
  where
    go :: forall local_t. LiftsFromClass f local_t => f local_t -> LiftsFrom f local_t
    go funs = case witness @f @local_t of
      LiftsFromNil -> funs
      LiftsFromFun -> \ list1 -> go (funs <*> list1)

fun1 :: Int -> Bool -> Double
fun1 x True = fromIntegral x + 3.14
fun1 x False = fromIntegral x + 2.78

fun2 :: Char -> Bool -> String -> Int
fun2 c b s = length (show c ++ show b ++ show s)

-- example1 :: [Double]
example1 = lift fun1 [1,2,3] [True, False, True]

-- example2 :: [Int]
example2 = lift fun2 "abc" [True, False, True] ["hello", "goodbye", "hi"]

-- example3 :: [Int]
example3 = lift ((+) @Int) [1,2,3] [4,5,6]

ZipWith.hs

{-# LANGUAGE AllowAmbiguousTypes #-}

-- Works, but bad type inference
module ZipWith where

import Prelude hiding (zipWith)
import qualified Prelude
import Data.Kind

class Lift f a r where
  lift :: a -> r
  ap :: Applicative f => f a -> r

instance {-# OVERLAPPABLE #-} Applicative f => Lift f a (f a) where
  lift = pure
  ap = id

instance {-# OVERLAPPING #-} (Applicative f, Lift f b r) => Lift f (a -> b) (f a -> r) where
  lift f fx = ap (f <$> fx)
  ap ff fx = ap (ff <*> fx)

class ZipWith a r where
  zipWith :: a -> r
  zipAp :: [a] -> r

instance {-# OVERLAPPABLE #-} ZipWith a [a] where
  zipWith = repeat
  zipAp = id

instance {-# OVERLAPPING #-} ZipWith b r => ZipWith (a -> b) ([a] -> r) where
  zipWith f fx = zipAp (f <$> fx)
  zipAp ff fx = zipAp (Prelude.zipWith ($) ff fx)