An implementation of an "apply" type-class which allows for overloading "function application".

Apply.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
module Apply where

import Prelude hiding ((++))


-- * Apply type-class

class Apply a b c where
  app :: a -> b -> c

instance Apply (a -> b) a b where
  app = ($)

instance Apply a (a -> b) b where
  app = flip ($)


-- * Ambiguous values

data List (k :: *) where
  LNil    :: List k
  LCons   ::      k -> List k -> List k
  LConcat :: List k -> List k -> List k

data Amb' (xs :: List *) where
  Nil    :: Amb' LNil
  Cons   ::      x  -> Amb' xs -> Amb' (LCons x xs)
  Concat :: Amb' xs -> Amb' ys -> Amb' (LConcat xs ys)

class AmbAppR f xs ys where
  ambappr :: f -> Amb' xs -> Amb' ys

instance AmbAppR f LNil LNil where
  ambappr _ Nil = Nil

instance (Apply f x y, AmbAppR f xs ys)
         => AmbAppR f (LCons x xs) (LCons y ys) where
  ambappr f (Cons x xs) = Cons (app f x) (ambappr f xs)

instance (AmbAppR f xs ys) => Apply f (Amb' xs) (Amb' ys) where
  app = ambappr


class AmbAppL fs x ys where
  ambappl :: Amb' fs -> x -> Amb' ys

instance AmbAppL LNil x LNil where
  ambappl Nil _ = Nil

instance (Apply f x y, AmbAppL fs x ys)
         => AmbAppL (LCons f fs) x (LCons y ys) where
  ambappl (Cons f fs) x = Cons (app f x) (ambappl fs x)

instance (AmbAppL fs x ys) => Apply (Amb' fs) x (Amb' ys) where
  app = ambappl


class AmbApp fs xs ys where
  ambapp :: Amb' fs -> Amb' xs -> Amb' ys

instance AmbApp LNil xs LNil where
  ambapp Nil _ = Nil

instance AmbApp fs LNil LNil where
  ambapp _ Nil = Nil

instance (AmbAppR f xs ys1, AmbApp fs xs ys2)
         => AmbApp (LCons f fs) xs (LConcat ys1 ys2) where
  ambapp (Cons f fs) xs = Concat (ambappr f xs) (ambapp fs xs)

instance (AmbApp fs xs ys) => Apply (Amb' fs) (Amb' xs) (Amb' ys) where
  app = ambapp


type family (xs :: [k]) :++ (ys :: [k]) :: [k] where
  '[] :++ ys = ys
  (x ': xs) :++ ys = x ': (xs :++ ys)

type family ToList (xs :: List k) :: [k] where
  ToList (LNil) = '[]
  ToList (LCons x xs) = x ': ToList xs
  ToList (LConcat xs ys) = ToList xs :++ ToList ys

type family FromList (xs :: [k]) :: List k where
  FromList '[] = LNil
  FromList (x ': xs) = LCons x (FromList xs)

type Amb xs = Amb' (FromList xs)


testval :: Amb '[Int, Double]
testval = Cons 1 (Cons 2 Nil)

testfun :: Amb '[Int -> Int, Double -> Double]
testfun = Cons (+1) (Cons (+2) Nil)

testapp :: Amb '[Int]
testapp = app ((+1) :: Int -> Int) testval


-- Ah, right. So basically I'm going to have to write out a
-- type-level function which decides if application is possible, and
-- then use this function to guide the instance search. Jolly.