SKI

ski.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module SkiTypes where

import Data.Proxy

data I -- I think the assumption is x is of kind *, but we want x of any arity.
-- We want to curry data constructors
data K
data S

data Nil
data Cons x xs

class First xs x | xs -> x
instance First Nil Nil
instance First (Cons x xs) x

class ListConcat a b c | a b -> c
instance ListConcat Nil x x
instance (ListConcat as bs cs)
  => ListConcat (Cons a as) bs (Cons a cs)

class Reduce combs result  | combs -> result where
  reduction :: Proxy combs -> Proxy result
  reduction Proxy = Proxy
instance Reduce Nil Nil
instance Reduce I I
instance Reduce K K
-- instance Reduce (Cons K (Cons a Nil)) (Cons K (Cons a Nil))
instance (Reduce cs rs) => Reduce (Cons I cs) rs
-- instance (Reduce cs rs, Reduce cs c) => Reduce c rs
instance (Reduce cs rs) => Reduce (Cons K (Cons cs (Cons xs rest))) (Cons rs rest)

instance Reduce (Cons S (Cons a (Cons b c))) (Cons (Cons a c) (Cons b c))

almost works! This statement should evaluate to K

*SkiTypes> :t reduction (Proxy :: Proxy (Cons I (Cons S (Cons K (Cons S (Cons (Cons I K) Nil))))))
reduction (Proxy :: Proxy (Cons I (Cons S (Cons K (Cons S (Cons (Cons I K) Nil))))))
  :: Proxy
       (Cons
          (Cons K (Cons (Cons I K) Nil)) (Cons S (Cons (Cons I K) Nil)))