From 47f6fb93c62c11c3e9ea92f723f7a62e7f0b52f1 Mon Sep 17 00:00:00 2001 From: Julien Moutinho Date: Sun, 16 May 2021 03:59:25 +0200 Subject: [PATCH 1/1] init --- Examples.hs | 14 +++++++ Main.hs | 9 +++++ Makefile | 6 +++ Reify.hs | 93 +++++++++++++++++++++++++++++++++++++++++++++++ SemanticAlp.hs | 46 +++++++++++++++++++++++ SemanticEval.hs | 16 ++++++++ SemanticSplice.hs | 27 ++++++++++++++ Syntax.hs | 8 ++++ Tests.hs | 91 ++++++++++++++++++++++++++++++++++++++++++++++ TestsSplice.hs | 27 ++++++++++++++ 10 files changed, 337 insertions(+) create mode 100644 Examples.hs create mode 100644 Main.hs create mode 100644 Makefile create mode 100644 Reify.hs create mode 100644 SemanticAlp.hs create mode 100644 SemanticEval.hs create mode 100644 SemanticSplice.hs create mode 100644 Syntax.hs create mode 100644 Tests.hs create mode 100644 TestsSplice.hs diff --git a/Examples.hs b/Examples.hs new file mode 100644 index 0000000..776de87 --- /dev/null +++ b/Examples.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} -- To get polymorphic types without type annotations +module Examples where + +-- * Haskell terms to represent as a custom (G)ADT, String, +-- Identity, TH.CodeQ, or whatever... +-- They could perfectly well be "black boxes" in another Haskell module. +-- Their only constraint is to have only arguments whose type is *polymorphic* +-- (possibly with contraints or type parameters though). + +-- Note the beta-reductible 'w', it will be normalized-out. +e0 = \x y z -> x / y + y + 2 * z + (\w -> y) z + +-- Note that 'f' is a function: arguments can be functions. +e1 = \f x -> f x diff --git a/Main.hs b/Main.hs new file mode 100644 index 0000000..814774a --- /dev/null +++ b/Main.hs @@ -0,0 +1,9 @@ +module Main where +import qualified Tests +import qualified TestsSplice + +main = do + Tests.print_e0 + Tests.print_e1 + TestsSplice.print_e0 + TestsSplice.print_e1 diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..8214944 --- /dev/null +++ b/Makefile @@ -0,0 +1,6 @@ +all: + runhaskell Main.hs +ghcid: + ghcid -c 'ghci Main.hs -ignore-dot-ghci -package template-haskell' --reverse-errors +ghci: + ghci -package template-haskell Main.hs diff --git a/Reify.hs b/Reify.hs new file mode 100644 index 0000000..477e4e5 --- /dev/null +++ b/Reify.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} -- For InferRR +{-# LANGUAGE FlexibleInstances #-} -- For InferRR +{-# LANGUAGE MultiParamTypeClasses #-} -- For InferRR +{-# LANGUAGE ScopedTypeVariables #-} -- For InferRR +{-# LANGUAGE TemplateHaskell #-} -- For reifyTH +{-# LANGUAGE TypeFamilies #-} -- For InferRR +{-# LANGUAGE UndecidableInstances #-} -- For InferRR +-- | Reify an Haskell value using type-directed normalisation-by-evaluation (NBE). +module Reify where + +import qualified Language.Haskell.TH as TH +import Syntax + + +-- | 'RR' witnesses the duality between @meta@ and @(repr a)@. +-- It indicates which type variables in @a@ are not to be instantiated +-- with the arrow type, and instantiates them to @(repr _)@ in @meta@. +-- This is directly taken from: http://okmij.org/ftp/tagless-final/course/TDPE.hs +-- +-- * @meta@ instantiates polymorphic types of the original Haskell expression +-- with @(repr _)@ types, according to how 'RR' is constructed +-- using 'base' and @('-->')@. This is obviously not possible +-- if the orignal expression uses monomorphic types (like 'Int'), +-- but remains possible with constrained polymorphic types (like @(Num i => i)@), +-- because @(i)@ can still be inferred to @(repr _)@, +-- whereas the finally chosen @(repr)@ +-- (eg. 'E', or 'Identity', or 'TH.CodeQ', or ...) +-- can have a 'Num' instance. +-- * @(repr a)@ is the symantic type as it would have been, +-- had the expression been written with explicit 'lam's +-- instead of bare haskell functions. +-- DOC: http://okmij.org/ftp/tagless-final/cookbook.html#TDPE +-- DOC: http://okmij.org/ftp/tagless-final/NBE.html +-- DOC: https://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf +data RR repr meta a = RR + { -- | 'reflect' converts from a *represented* Haskell term of type @a@ + -- to an object *representing* that value of type @a@. + reify :: meta -> repr a + -- | 'reflect' converts back an object *representing* a value of type @a@, + -- to the *represented* Haskell term of type @a@. + , reflect :: repr a -> meta + } + +-- | The base of induction : placeholder for a type which is not the arrow type. +base :: RR repr (repr a) a +base = RR{reify = id, reflect = id} + +-- | The inductive case : the arrow type. +-- 'reify' and 'reflect' are built together inductively. +infixr 8 --> +(-->) :: Abstractable repr => + RR repr m1 o1 -> RR repr m2 o2 -> + RR repr (m1 -> m2) (o1 -> o2) +r1 --> r2 = RR + { reify = \meta -> lam (reify r2 . meta . reflect r1) + , reflect = \repr -> reflect r2 . (.@) repr . reify r1 + } + + +-- * Using a type-class to partially infer 'RR' + +-- | Try to infer 'RR' from 'meta' and @(a)@. +-- Using 'inferRR' will still require a type annotation, +-- though it can often be partial. +class InferRR repr meta a where + inferRR :: RR repr meta a +instance {-# OVERLAPPING #-} + ( InferRR repr m1 a1 + , InferRR repr m2 a2 + , Abstractable repr + ) => InferRR repr (m1 -> m2) (a1 -> a2) where + inferRR = inferRR --> inferRR +instance {-# OVERLAPPABLE #-} + p ~ repr a => + InferRR repr p a where inferRR = base + +reifyImplicit :: InferRR repr meta a => meta -> repr a +reifyImplicit = reify inferRR + + +-- * Using TemplateHaskell to fully auto-generate 'RR' + +-- | @$(reifyTH 'Foo.bar)@ calls 'reify' on 'Foo.bar' +-- with an 'RR' generated from the infered type of 'Foo.bar'. +reifyTH :: TH.Name -> TH.Q TH.Exp +reifyTH name = do + info <- TH.reify name + case info of + TH.VarI n (TH.ForallT _vs _ctx ty) _dec -> + [| reify $(genRR ty) $(return (TH.VarE n)) |] + where + genRR (TH.AppT (TH.AppT TH.ArrowT a) b) = [| $(genRR a) --> $(genRR b) |] + genRR TH.VarT{} = [| base |] diff --git a/SemanticAlp.hs b/SemanticAlp.hs new file mode 100644 index 0000000..ad350a3 --- /dev/null +++ b/SemanticAlp.hs @@ -0,0 +1,46 @@ +-- | Semantics for Alp's Expr +module SemanticAlp where + +import Syntax +import qualified Control.Monad.State.Strict as MT + +-- | An untyped expression. +-- This is only to keep Alp's initial algebra for the demo. +-- Would require a GADT to enforce type-preservation. +-- Would require to be replaced by final algebras (like 'Abstractable') to stay extensible, +-- at the cost of pattern-matchability, though it could be recovered +-- by using an existentialized data family indexed by the syntax type-classes. +-- Though there are 'V'ariables, there is no lambda constructor in this 'Expr', +-- but one could be added if wanted, then 'MT.State' could be replaced +-- by 'MT.Reader' to use DeBruijn indices instead of a global counter +-- (not necessarily quicker though). +data Expr v k = K k | V v | Unop Unop (Expr v k) | Binop Binop (Expr v k) (Expr v k) + deriving (Show) +data Unop = Negate | Abs | Signum | FromInteger | Inv + deriving (Show) +data Binop = Add | Mul | Sub | Div | App {- added to support (.@) -} + deriving (Show) + +-- * An example of representation : generating an 'Expr' + +data E a = E { unE :: MT.State Int (Expr Int Float) } +compile :: E a -> Expr Int Float +compile = (`MT.evalState` 0) . unE +instance Abstractable E where + f .@ x = E $ Binop App <$> unE f <*> unE x + lam f = E $ do + v <- MT.get + MT.put (succ v) + unE (f (E (return (V v)))) +instance Num a => Num (E a) where + x + y = E $ Binop Add <$> unE x <*> unE y + x * y = E $ Binop Mul <$> unE x <*> unE y + x - y = E $ Binop Sub <$> unE x <*> unE y + abs x = E $ Unop Abs <$> unE x + signum x = E $ Unop Signum <$> unE x + fromInteger i = E $ return (K (fromInteger i)) + negate x = E $ Unop Negate <$> unE x +instance Fractional a => Fractional (E a) where + fromRational r = E $ return (K (fromRational r)) + recip x = E $ Unop Inv <$> unE x + x / y = E $ Binop Div <$> unE x <*> unE y diff --git a/SemanticEval.hs b/SemanticEval.hs new file mode 100644 index 0000000..a20b605 --- /dev/null +++ b/SemanticEval.hs @@ -0,0 +1,16 @@ +-- | Semantics for Identity (aka. R, or meta-circular representation). +module SemanticEval where + +import Data.Functor.Identity +import Syntax + +instance Abstractable Identity where + lam f = Identity (runIdentity . f . Identity) + (.@) f x = Identity ((runIdentity f) (runIdentity x)) +{- Defined in Data.Functor.Identity +instance Num a => Num (Identity a) +instance Fractional a => Fractional (Identity a) +-} + +eval :: Identity a -> a +eval = runIdentity diff --git a/SemanticSplice.hs b/SemanticSplice.hs new file mode 100644 index 0000000..fc7f198 --- /dev/null +++ b/SemanticSplice.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TemplateHaskell #-} +-- | Semantics for TemplateHaskell +module SemanticSplice where + +import qualified Language.Haskell.TH as TH +import qualified Language.Haskell.TH.Syntax as TH +import Syntax + +instance Abstractable (TH.Code TH.Q) where + lam f = [|| \x -> $$(f [||x||]) ||] + (.@) f x = [|| $$f $$x ||] +instance Num a => Num (TH.Code TH.Q a) where + x + y = [|| $$x + $$y ||] + x * y = [|| $$x * $$y ||] + x - y = [|| $$x - $$y ||] + abs x = [|| abs $$x ||] + signum x = [|| signum $$x ||] + fromInteger i = [|| fromInteger $$(TH.liftTyped i) ||] + negate x = [|| $$x ||] +instance Fractional a => Fractional (TH.Code TH.Q a) where + fromRational i = [|| fromRational $$(TH.liftTyped i) ||] + recip x = [|| recip $$x ||] + x / y = [|| $$x / $$y ||] + +splice :: TH.CodeQ a -> IO String +splice q = TH.runQ (TH.examineCode q) >>= return . TH.pprint . TH.unType diff --git a/Syntax.hs b/Syntax.hs new file mode 100644 index 0000000..41f8347 --- /dev/null +++ b/Syntax.hs @@ -0,0 +1,8 @@ +module Syntax where + +-- | Usual syntax for type-preserving term-abstraction. +class Abstractable repr where + -- | Lambda term (abstract). + lam :: (repr a -> repr b) -> repr (a -> b) + -- | Term application (unabstract). + (.@) :: repr (a -> b) -> repr a -> repr b; infixl 9 .@ diff --git a/Tests.hs b/Tests.hs new file mode 100644 index 0000000..e76b696 --- /dev/null +++ b/Tests.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} -- +{-# LANGUAGE FlexibleContexts #-} -- +{-# LANGUAGE TupleSections #-} -- Convenience +{-# LANGUAGE AllowAmbiguousTypes #-} -- For using reifyImplicit +{-# LANGUAGE TypeApplications #-} -- For using reifyImplicit +{-# LANGUAGE TemplateHaskell #-} -- For using reifyTH +module Tests where + +import qualified Examples +import Reify +import SemanticAlp as Alp +import SemanticSplice +import SemanticEval + +-- * Reifying 'Examples.e0' +e0_ReprExplicit = reify (base-->base-->base-->base) Examples.e0 +e0_ReprImplicit = reifyImplicit Examples.e0 +e0_ReprTemplate = $(reifyTH 'Examples.e0) +-- e0_ReprExplicit, e0_ReprImplicit, e0_ReprTemplate :: +-- (Syntax.Abstractable repr, Fractional (repr o2)) => +-- repr (o2 -> o2 -> o2 -> o2) +-- Note: @repr@ is polymorphic, hence those representations +-- can be instantiated to many syntaxes. + +-- ** First syntax +e0_ExprExplicit = Alp.compile e0_ReprExplicit +-- | 'inferRR' can't infer that the last polymorphic type +-- must not be the arrow-type. +-- | 'inferRR' can't infer that 'o2' is not the arrow type. +e0_ExprImplicit = Alp.compile @(_ -> _ -> _ -> Float) e0_ReprImplicit +-- | But 'reifyTH' can. +e0_ExprTemplate = Alp.compile e0_ReprTemplate + +-- ** Second syntax +e0_EvalExplicit = eval e0_ReprExplicit +e0_EvalImplicit = eval @(_ -> _ -> _ -> Float) e0_ReprImplicit +e0_EvalTemplate = eval e0_ReprTemplate + +-- ** Third syntax +e0_SpliceExplicit = splice e0_ReprExplicit +e0_SpliceImplicit = splice @(_ -> _ -> _ -> Float) e0_ReprImplicit +e0_SpliceTemplate = splice e0_ReprTemplate + +print_e0 = do + print ("e0_ExprExplicit", e0_ExprExplicit) + print ("e0_ExprImplicit", e0_ExprImplicit) + print ("e0_ExprTemplate", e0_ExprTemplate) + print ("e0_EvalExplicit 1 2 3", e0_EvalExplicit 1 2 3) + print ("e0_EvalImplicit 1 2 3", e0_EvalImplicit 1 2 3) + print ("e0_EvalTemplate 1 2 3", e0_EvalTemplate 1 2 3) + print =<< ("e0_SpliceExplicit",) <$> e0_SpliceExplicit + print =<< ("e0_SpliceImplicit",) <$> e0_SpliceImplicit + print =<< ("e0_SpliceTemplate",) <$> e0_SpliceTemplate + +-- * Reifying 'Examples.e1' +e1_ReprExplicit = reify ((base-->base)-->base-->base) Examples.e1 +e1_ReprImplicit = reifyImplicit Examples.e1 +e1_ReprTemplate = $(reifyTH 'Examples.e1) +-- e1_ReprExplicit, e1_ReprImplicit, e1_ReprTemplate :: +-- Syntax.Abstractable repr => +-- repr ((o1 -> o2) -> o1 -> o2) + +-- ** First syntax +e1_ExprExplicit = Alp.compile e1_ReprExplicit +-- | 'inferRR' can't infer 'o1' and 'o2' aren't the arrow type. +e1_ExprImplicit = Alp.compile @((_ -> _) -> Float -> Float) e1_ReprImplicit +-- | But 'reifyTH' can. +e1_ExprTemplate = Alp.compile e1_ReprTemplate + +-- ** Second syntax +e1_EvalExplicit = eval e1_ReprExplicit +-- | 'inferRR' can't keep the function polymorphic. +e1_EvalImplicit = eval @((_ -> _) -> Float -> Float) e1_ReprImplicit +-- | But 'reifyTH' can. +e1_EvalTemplate = eval e1_ReprTemplate + +-- ** Third syntax +e1_SpliceExplicit = splice e1_ReprExplicit +e1_SpliceImplicit = splice @((_ -> _) -> Float -> Float) e1_ReprImplicit +e1_SpliceTemplate = splice e1_ReprTemplate + +print_e1 = do + print ("e1_ExprExplicit", e1_ExprExplicit) + print ("e1_ExprImplicit", e1_ExprImplicit) + print ("e1_ExprTemplate", e1_ExprTemplate) + print ("e1_EvalExplicit id 42", e1_EvalExplicit id 42) -- 42 + print ("e1_EvalImplicit id 42", e1_EvalImplicit id 42) -- 42.0 + print ("e1_EvalTemplate id 42", e1_EvalTemplate id 42) -- 42 + print =<< ("e1_SpliceExplicit",) <$> e1_SpliceExplicit + print =<< ("e1_SpliceImplicit",) <$> e1_SpliceImplicit + print =<< ("e1_SpliceTemplate",) <$> e1_SpliceTemplate diff --git a/TestsSplice.hs b/TestsSplice.hs new file mode 100644 index 0000000..f6fa3ec --- /dev/null +++ b/TestsSplice.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} +module TestsSplice where + +import qualified Language.Haskell.TH as TH +import Reify +import Tests +import qualified Examples + +e0_SplicedImplicit = $$(e0_ReprImplicit :: TH.CodeQ (_ -> _ -> _ -> Float)) +e0_SplicedTemplate = $$(e0_ReprTemplate) +e0_SplicedTemplateDirect = $$($(reifyTH 'Examples.e0)) + +print_e0 = do + print ("e0_SplicedImplicit 1 2 3", e0_SplicedImplicit 1 2 3) + print ("e0_SplicedTemplate 1 2 3", e0_SplicedTemplate 1 2 3) + print ("e0_SplicedTemplateDirect 1 2 3", e0_SplicedTemplateDirect 1 2 3) + +e1_SplicedImplicit = $$(e1_ReprImplicit :: TH.CodeQ ((_ -> _) -> Float -> Float)) +e1_SplicedTemplate = $$(e1_ReprTemplate) +e1_SplicedTemplateDirect = $$($(reifyTH 'Examples.e1)) + +print_e1 = do + print ("e1_SplicedImplicit id 42", e1_SplicedImplicit id 42) -- 42.0 + print ("e1_SplicedTemplate id 42", e1_SplicedTemplate id 42) -- 42 + print ("e1_SplicedTemplateDirect id 42", e1_SplicedTemplateDirect id 42) -- 42 -- 2.47.0