diff --git a/Guess/Combinator.hs b/Guess/Combinator.hs
new file mode 100644
--- /dev/null
+++ b/Guess/Combinator.hs
@@ -0,0 +1,175 @@
+{-# LANGUAGE
+  UndecidableInstances,
+  UnicodeSyntax, TypeOperators, ScopedTypeVariables, MultiParamTypeClasses,
+  FunctionalDependencies, TypeSynonymInstances, FlexibleInstances, 
+  FlexibleContexts, NoMonomorphismRestriction #-}
+
+module Guess.Combinator (combinator) where
+
+-- ^ Guess a value for a combinator
+-- 
+-- Based on De-typechecker: converting from a type to a term
+-- by <oleg at pobox.com>
+-- http://www.haskell.org/pipermail/haskell/2005-March/015423.html
+
+import Guess.Combinator.Lib
+
+-- | Guess a combinator given its type
+-- 
+-- Example:
+-- 
+-- >>> let f = combinator :: (b -> c) -> (a -> b) -> a -> c
+-- >>> f (:[]) ((,) True) 10
+-- [(True, 10)]
+
+combinator ∷ GuessCombinator t HNil ⇒ t
+combinator = combinatorWith emptyEnv
+
+-- | Tests
+test =
+  ((combinator ∷ a → (a → b) → b) 'O' (:"K"), "OK")
+  .*. (combinator 'O' (:"K") :: String, "OK")
+  .*. ((combinator ∷ a → (a → b) → b) 1 (+2), 3)
+  .*. ((combinator ∷ (b → c) → (a → b) → a → c) Just Right True, Just (Right True))
+  .*. ((combinator ∷ a → b → a) 'a' 'b', 'a')
+  .*. ((combinator ∷ (t → t1) → t → t2 → t1) Just 1 'c', Just 1)
+  .*. ((combinator ∷ (b → c) → (a → b) → a → c) (:[]) ((,) True) 10, [(True, 10)])
+  .*. ((combinator ∷ (((a → b → c) → (a → b) → a → c)→ (t3 → t1 → t2 → t3) → t) → t) (\f g → f (g 1) (:[]) 2), 1)
+  .*. ((combinator ∷ ((a → b) → c) → (a → b) → c) ($2) (+3), 5)
+  .*. (combinator 'a' True ∷ Bool, True) 
+  .*. HNil
+
+-- | A type/value pair
+-- 
+-- The list representation of the type is also kept.
+
+newtype TypeToTermT tl t = TypeToTermT t deriving Show
+
+-- | GuessCombinator +type +env
+-- Guess a combinator given its type and an environment
+
+class GuessCombinator t env where
+    combinatorWith ∷ env → t
+
+instance (IsFunction t flag,
+          GuessWith' flag t env)
+       ⇒ GuessCombinator t env where
+    combinatorWith = guessWith' (Proxy ∷ Proxy flag)
+
+class GuessWith' flag t env where
+    guessWith' ∷ (Proxy flag) → env → t
+
+-- | If its a function, add the argument to the environment and guess the result
+instance (IsFunction x flagx,
+          FunToList' flagx x tlx, 
+          IsFunction y flagy,
+          GuessWith' flagy y ((TypeToTermT tlx x) :*: env))
+       ⇒ GuessWith' HTrue (x → y) env where
+  guessWith' _ env = \(v ∷ x) →
+             guessWith' (Proxy ∷ Proxy flagy) (((TypeToTermT v) ∷ TypeToTermT tlx x) .*. env)
+
+-- | If it's not a function, let RResolve find a suitable value
+instance (RResolve env ((t :*: HNil) :*: HNil) HNil t)
+       ⇒ GuessWith' HFalse t env where
+    guessWith' _ env = rresolve env (Proxy ∷ Proxy ((t :*: HNil) :*: HNil)) HNil
+
+-- | RResolve +env +goals +retlist -ret
+-- Type-level SLD resolution algorithm
+-- 
+-- env: a list of TypeToTermT
+-- goals: the tail of a flattened type
+-- retlist: a function and arguments, reversed, such as any one of tails [a, b, b -> a -> ret]
+-- ret: resulting type/value (a collapsed retlist)
+
+class RResolve env goals tl t | env goals tl → t where
+    rresolve ∷ env → (Proxy goals) → tl → t
+
+-- | When there are no goals left and the retlist is a singleton, return it
+
+instance RResolve env HNil (t :*: HNil) t where
+    rresolve _ _ (HCons t HNil) = t
+
+-- | When there are no goals left and the retlist is not a singleton, collapse the retlist
+
+instance RResolve env HNil (t1 :*: tr) (t→r)
+       ⇒ RResolve env HNil (t :*: t1 :*: tr) r where
+    rresolve g _ (HCons t r) = (rresolve g (Proxy ∷ Proxy HNil) r) t
+
+-- | When the type we want is not a function, look it up in the environment.
+-- If we have a function that returns it, save the function and guess its arguments.
+
+instance (RHLookup g env (TypeToTermT (g :*: assum) g'),
+          HReverse assum assum',
+          RResolve env assum' (g' :*: HNil) ra,
+          RResolve env gr (ra :*: pt) t)
+       ⇒ RResolve env ((g :*: HNil) :*: gr) pt t where
+    rresolve env _ pt = rresolve env (Proxy ∷ Proxy gr) (ra .*. pt)
+     where
+      TypeToTermT t1 = rhlookup (Proxy ∷ Proxy g) env
+      ra ∷ ra = rresolve env (Proxy ∷ Proxy assum') (t1 .*. HNil)
+
+-- | The instance for improper combinators was left as an exercise.
+-- 
+-- When we need a function, build the function, add its arguments to the
+-- environment and guess the result.
+
+instance (HReverse (gc :*: gcr) revr,
+          ExtendEnv env revr ra env' f,
+          RResolve env' ((g :*: HNil) :*: HNil) HNil ra,
+          RResolve env gr (f :*: pt) t)
+         ⇒ RResolve env ((g :*: gc :*: gcr) :*: gr) pt t where
+  rresolve (env ∷ env) _ (pt ∷ pt) = rresolve env (Proxy ∷ Proxy gr) (f .*. pt)
+    where
+      f ∷ f
+      f = extendEnv env (Proxy ∷ Proxy revr) $ \(env' ∷ env') →
+          rresolve env' (Proxy ∷ Proxy ((g :*: HNil) :*: HNil)) HNil
+
+-- | Extend an environment with the arguments of a function.
+-- 
+-- The argument list must be the reverse of the tail of the flattened
+-- function type.
+-- 
+-- Given a continutation, return a function that builds the environment.
+-- For example: 
+-- extendEnv [] [[a] [b]] k = \a b -> k env'
+
+class ExtendEnv env vs ret env' fun | env vs ret → env' fun where
+  extendEnv ∷ env → (Proxy vs) → (env' → ret) → fun
+
+instance ExtendEnv env HNil ret env ret where
+  extendEnv env _ k = k env
+  
+instance
+  (ExtendEnv env rest ret env' fun,
+   ListToFun pt t)
+  ⇒ ExtendEnv env (pt :*: rest) ret ((TypeToTermT pt t) :*: env') (t → fun)
+   where 
+ extendEnv env _ f = \(t ∷ t) →
+   extendEnv env (Proxy ∷ Proxy rest) $ \env' →
+   f ((TypeToTermT t ∷ TypeToTermT pt t) .*. env')
+
+-- | Lookup in the `associative' type-indexed list
+
+class RHLookup t l w | t l → w where
+    rhlookup ∷ (Proxy t) → l → w
+
+instance (TypeEq t t' flag, RHLookup' flag t ((TypeToTermT (t' :*: at) tt') :*: r) w)
+    ⇒ RHLookup t ((TypeToTermT (t' :*: at) tt') :*: r) w where
+    rhlookup = rhlookup' (Proxy ∷ Proxy flag)
+
+class RHLookup' flag t l w | flag t l → w where
+    rhlookup' ∷ (Proxy flag) → (Proxy t) → l → w
+
+instance RHLookup' HTrue t ((TypeToTermT (t :*: at) tt) :*: r) 
+                            (TypeToTermT (t :*: at) tt) where
+    rhlookup' _ _ (HCons t _) = t
+
+instance RHLookup t r w ⇒ RHLookup' HFalse t ((TypeToTermT tl' t') :*: r) w where
+    rhlookup' _ t (HCons _ r) = rhlookup t r
+
+-- | An empty environment.
+emptyEnv = HNil
+
+-- | Add a type/value to the environment
+consEnv ∷ FunToList t tl ⇒ t → env → TypeToTermT tl t :*: env
+consEnv x env = TypeToTermT x .*. env
diff --git a/Guess/Combinator/Lib.hs b/Guess/Combinator/Lib.hs
new file mode 100644
--- /dev/null
+++ b/Guess/Combinator/Lib.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE
+  UndecidableInstances, IncoherentInstances,
+  UnicodeSyntax, TypeOperators, ScopedTypeVariables, MultiParamTypeClasses,
+  FunctionalDependencies, TypeSynonymInstances, FlexibleInstances, 
+  FlexibleContexts #-}
+
+module Guess.Combinator.Lib (module Prelude, module Data.HList, module Guess.Combinator.Lib) where
+
+import Prelude (($), (++), show, Either(..), Maybe(..), Num(..), Show(..), Bool(..))
+import Data.HList (HTrue, HFalse, HNil(HNil), HCons(HCons), (:*:), HAppend, HReverse)
+import Data.HList.TypeCastGeneric2 (TypeCast)
+
+-- | FunToList +type -typelist
+-- Flatten the functions in a given type, in reverse order
+-- 
+-- For example, FunToList (a -> (b -> c) -> d) [d, [c, [b]], [a]]
+
+class FunToList t tl | t → tl
+
+instance (IsFunction t flag,
+          FunToList' flag t tl)
+         ⇒ FunToList t tl
+
+class FunToList' a t tl | a t → tl
+
+instance FunToList' HFalse t (t :*: HNil)
+
+instance (FunToList x tlx,
+          FunToList y tly,
+          HAppend tly (tlx :*: HNil) tl) 
+       ⇒ FunToList' HTrue (x → y) tl
+
+-- | ListToFun +typelist -type
+-- 
+-- Reverse of FunToList
+
+class ListToFun tl t | tl → t
+
+instance ListToFun (t :*: HNil) t
+
+instance (ListToFun tl a,
+          ListToFun ((a → r) :*: tls) t)
+         ⇒ ListToFun (r :*: (tl :*: tls)) t
+
+-- Misc type-level programming classes and helpers
+
+infixr 2 .*.
+a .*. b = HCons a b
+
+class IsFunction a b | a → b
+instance TypeCast f HTrue ⇒ IsFunction (x → y) f
+instance TypeCast f HFalse ⇒ IsFunction a f
+
+class TypeEq' () x y b ⇒ TypeEq x y b | x y → b
+class TypeEq' q x y b | q x y → b
+class TypeEq'' q x y b | q x y → b
+instance TypeEq' () x y b ⇒ TypeEq x y b
+instance TypeCast b HTrue ⇒ TypeEq' () x x b
+instance TypeEq'' q x y b ⇒ TypeEq' q x y b
+instance TypeEq'' () x y HFalse
+
+data Proxy t = Proxy
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2012, Etienne Laurin
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the
+   distribution.
+
+3. Neither the name of the copyright holder nor the names of other
+   contributors may be used to endorse or promote products derived
+   from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,5 @@
+module Main (main) where
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/guess-combinator.cabal b/guess-combinator.cabal
new file mode 100644
--- /dev/null
+++ b/guess-combinator.cabal
@@ -0,0 +1,21 @@
+Name:                guess-combinator
+Version:             0.1
+Synopsis:            Generate simple combinators given their type
+description:         Based on De-typechecker: converting from a type to a term
+                     by <oleg at pobox.com>
+                     http://www.haskell.org/pipermail/haskell/2005-March/015423.html
+Homepage:            http://code.atnnn.com/project/guess
+License:             BSD3
+License-file:        LICENSE
+Author:              Etienne Laurin
+Maintainer:          Etienne Laurin <etienne@atnnn.com>
+Category:            Development
+Build-type:          Simple
+Cabal-version:       >=1.2
+
+
+Library
+  Exposed-modules: Guess.Combinator
+  Build-depends: HList,
+                 base >= 2 && < 5
+  Other-modules: Guess.Combinator.Lib