packages feed

guess-combinator (empty) → 0.1

raw patch · 5 files changed

+293/−0 lines, 5 filesdep +HListdep +basesetup-changed

Dependencies added: HList, base

Files

+ Guess/Combinator.hs view
@@ -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
+ Guess/Combinator/Lib.hs view
@@ -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
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,5 @@+module Main (main) where+import Distribution.Simple++main :: IO ()+main = defaultMain
+ guess-combinator.cabal view
@@ -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