Last active
August 29, 2015 14:05
-
-
Save wenkokke/75aa1815e364555937a5 to your computer and use it in GitHub Desktop.
An implementation of an "apply" type-class which allows for overloading "function application".
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment