diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for fcf-family + +## 0.1.0.0 -- 2023-01-23 + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2022 Li-yao Xia + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,91 @@ +# Family of families: featherweight defunctionalization + +## Motivation + +This package transforms regular type families into +["first-class families"](https://hackage.haskell.org/package/first-class-families). +It does so without declaring dummy data types as defunctionalization symbols, +avoiding namespace pollution. + +### Featherweight defunctionalization + +The idea is to use strings. There is an unambiguous way to refer to an existing type family: +by its fully qualified name---a triple of a package name, module name, and base name. + +```haskell +GHC.TypeNats.+ +-- as a Name -- +MkName "base" "GHC.TypeNats" "+" +``` + +All type families can be promoted to first-class using a single symbol indexed by +qualified names. That is the `Family` of type families. + +- No namespace pollution: Promoting a type family requires no new data type, + only an `Eval` instance for its name. +- Decentralization: Every type family induces a unique `Eval` instance, + and multiple packages may declare the same instance without conflicts. + +```haskell +type instance Eval (Family_ (MkName "base" "GHC.TypeNats" "+") _ '(x, '(y, '()))) = x + y +``` + +For more details on this encoding, see the module `Fcf.Family`. + +## Usage + +### Promote a type family + +To promote a type family, the necessary boilerplate +can be generated with Template Haskell, using the function `Fcf.Family.TH.fcfify`. + +```haskell +fcfify ''MyTypeFamily + +-- Examples +fcfify ''(GHC.TypeNats.+) +fcfify ''Data.Type.Bool.If +``` + +This generates instances of `Eval` and auxiliary type families for that former +instance to be well-defined. + +### Use the promoted type family + +This allows using the defunctionalization symbol `Family` indexed by the +type family's name---a tuple of strings constructed with `MkName`. + +```haskell + Eval (Family (MkName "base" "GHC.TypeNats" "+") P0 '(1, '(2, '()))) += 1 + 2 += 3 + + Eval (Family (MkName "base" "GHC.Type.Bool" "If") P1 '( 'True, '("yes", '("no", '())))) += If 'True "yes" "no" += "yes" +``` + +The `familyName` function converts the name of an actual family to an *fcf-family* name in Template Haskell. + +```haskell + Eval (Family $(familyName ''+) P0 '(1, '(2, '()))) += 3 + + Eval (Family $(familyName ''If) P1 '( 'True, '("yes", '("no", '())))) += "yes" +``` + +## Existing instances + +- The library [`fcf-base`](https://hackage.haskell.org/package/fcf-base) contains instances for type families defined in *base*. +- The module `Fcf.Family.Meta` contains the instance for `Eval`. + +## Limitations + +- There is partial support for dependently typed type families. + The kind of the result may depend on its arguments. + This package does not yet support type families where the kind of arguments + depends on other visible arguments. +- Invisible arguments are currently all assumed to be of kind `Type`. + Lifting this restriction requires either access to more typing information + from the compiler via TH, or some implementation of kind inference in TH. diff --git a/fcf-family.cabal b/fcf-family.cabal new file mode 100644 --- /dev/null +++ b/fcf-family.cabal @@ -0,0 +1,46 @@ +cabal-version: 3.0 +name: fcf-family +version: 0.1.0.0 +synopsis: Family of families: featherweight defunctionalization +description: + Promote regular type families to first-class, + without polluting the type namespace. + . + See README. +homepage: https://gitlab.com/lysxia/fcf-family +license: MIT +license-file: LICENSE +author: Li-yao Xia +maintainer: lysxia@gmail.com +category: Other +build-type: Simple +extra-doc-files: CHANGELOG.md, README.md +tested-with: GHC == { 9.0.2, 9.2.2, 9.4.1 } + +common warnings + ghc-options: -Wall + +library + import: warnings + exposed-modules: + Fcf.Family + Fcf.Family.Meta + Fcf.Family.TH + build-depends: + first-class-families, + containers, + template-haskell, + base >=4.15 && < 4.20 + hs-source-dirs: src + default-language: Haskell2010 + +test-suite fcf-family-test + import: warnings + default-language: Haskell2010 + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Main.hs + build-depends: + base, + first-class-families, + fcf-family diff --git a/src/Fcf/Family.hs b/src/Fcf/Family.hs new file mode 100644 --- /dev/null +++ b/src/Fcf/Family.hs @@ -0,0 +1,301 @@ +{-# LANGUAGE + AllowAmbiguousTypes, + DataKinds, + PolyKinds, + RankNTypes, + ScopedTypeVariables, + StandaloneKindSignatures, + TypeFamilies, + TypeOperators, + UndecidableInstances #-} + +-- | +-- Description: The family of type families +-- +-- = The family of type families +-- +-- /fcf-family/ promotes +-- regular type families to first-class families without +-- defining new symbols (which would either pollute the type namespace +-- or require a centralized organization to decide where the symbol +-- for each family should be defined). +-- +-- Every type family is uniquely identified by its qualified 'Name': +-- package, module, and base name. +-- +-- Example names: +-- +-- @ +-- -- GHC.TypeNats.+ +-- 'MkName' \"base\" \"GHC.TypeNats\" \"+\" +-- +-- -- Data.Type.Bool.If +-- 'MkName' \"base\" \"Data.Type.Bool\" \"If\" +-- @ +-- +-- Hence, a single symbol 'Family' indexed by names +-- is sufficient to promote all regular type families. +-- +-- == Promoting a type family to first-class +-- +-- For example, the type family @('GHC.TypeNats.+')@ is promoted using the following +-- 'Eval' instance for 'Family': +-- +-- @ +-- type (::+) = 'MkName' \"base\" \"GHC.TypeNats\" \"+\" -- 'Name' of (+) +-- type instance 'Eval' ('Family_' (::+) _ '(x, '(y, '())))) = x 'GHC.TypeNats.+' y +-- @ +-- +-- The necessary instances can be generated using 'Fcf.Family.TH.fcfify' from the +-- module "Fcf.Family.TH". +-- +-- @ +-- 'Fcf.Family.TH.fcfify' \'\'+ +-- @ +-- +-- The name of the family can be quoted using 'Fcf.Family.TH.familyName'. +-- +-- @ +-- type (::+) = $(pure ('Fcf.Family.TH.familyName' \'\'+)) +-- @ +-- +-- Two modules may invoke 'Fcf.Family.TH.fcfify' on the same name without conflict. +-- Identical type family instances will be generated, which is allowed. +-- +-- Examples: +-- +-- @ +-- 2 'GHC.TypeNats.+' 3 +-- ~ +-- 'Eval' ('Family' ('MkName' \"base\" \"GHC.TypeNats\" \"+\") 'P0' '(2, '(3, '()))) +-- @ +-- +-- @ +-- 'Data.Type.Bool.If' a b c +-- ~ +-- 'Eval' ('Family' ('MkName' \"base\" \"Data.Type.Bool\" \"If\") 'P1' '(a, '(b, '(c, \())))) +-- @ +-- +-- == Details +-- +-- The type of 'Family' is an uncurried version of the original type family: +-- +-- @ +-- 'Family' (::+) _ :: (Nat, (Nat, ())) -> Exp Nat +-- ('GHC.TypeNats.+') :: Nat -> Nat -> Nat +-- @ +-- +-- Tuples @(,)@ and @()@ are used as the cons and nil of heterogeneous lists of arguments. +-- +-- The signature of the relevant family is encoded by implementing the following +-- type instances: +-- +-- @ +-- -- Auxiliary instances. +-- type instance 'Params' (::+) = () +-- type instance 'Args_' (::+) _ = (Nat, (Nat, ())) +-- type instance 'Res_' (::+) _ _ = Nat +-- @ +-- +-- 'Args_' and 'Res_' denote the types of arguments and result of the given type family. +-- 'Params' denotes the type of implicit parameters (there are none here +-- since @('GHC.TypeNats.+')@ is monomorphic). +-- The type of explicit arguments ('Args_') may depend on the implicit parameters ('Params'). +-- The result type ('Res_') may depend on both 'Params' and 'Args_'. +-- +-- === Untyped inside, typed outside #wrappers# +-- +-- These families are intended to be very dependent (the type of 'Family' depends on 'Res' depends on 'Args' depends on 'Params'). +-- However, the implementation of this library must work around some technical limitations of GHC. +-- 'Args_' and 'Res_' are actually "untyped" to make GHC more lenient in type +-- checking their instances. \"Typed\" wrappers, 'Family', 'Res', 'Args' are +-- then provided to invoke those families with their intended types, +-- which allows type inference to work. +-- +-- To recap: define instances of 'Params', 'Args_', 'Res_', 'Family_', +-- but to invoke the latter three, use 'Args', 'Res', and 'Family' instead. +-- +-- == Implicit parameters +-- +-- An example using implicit parameters is @'Data.Type.Bool.If' :: forall k. Bool -> k -> k -> k@. +-- +-- @ +-- type If_ = 'MkName' \"base\" \"Data.Type.Bool\" \"If\" +-- type instance 'Eval' ('Family_' If_ _ '(b, '(x, '(y, '())))) = 'Data.Type.Bool.If' b x y +-- +-- type instance 'Params' If_ = ('Data.Kind.Type', ()) -- Type of the implicit parameter +-- type instance 'Args_' If_ k = (Bool, (k, (k, ()) -- Types of the explicit arguments +-- type instance 'Res_' If_ k _ = k -- Type of the result +-- @ +-- +-- The second argument of 'Family_' is a proxy that carries the implicit parameters +-- in its type. For example, the type of @'Family' If_@ is really: +-- +-- @ +-- 'Family' If_ (_ :: Proxy k) :: (Bool, (k, (k, ()))) -> k +-- @ +-- +-- When using 'Family', apply it to a proxy encoding the number of implicit parameters +-- in unary using 'P0' and 'PS'. +-- +-- For example, use 'P0' for the monomorphic @('GHC.TypeNats.+')@ +-- and 'P1' (equal to @'PS' 'P0'@) for 'Data.Type.Bool.If'. + +module Fcf.Family + ( -- * Main definitions + + -- ** First-class families + -- $reexport + Exp + , Eval + + -- ** Family of families + , Name(..) + , Family + , Family_ + , NDFamily + , NDFamily_ + + -- ** Encoding type family signatures + -- $arity + , Params + , Args + , Args_ + , Res + , Res_ + + -- * Implicit parameters + -- $tuples + , ParamsProxy + , P0, P1, P2, P3, P4, P5, P6, P7 + , PS + + -- * Coercions + -- $hack + , Coerce, CoerceTo, CoerceFrom + , Transp + ) where + +import Data.Kind (Type) +import Data.Proxy (Proxy(..)) +import Data.Type.Equality ((:~:)(..)) +import GHC.Exts (Any) +import GHC.TypeLits (Symbol) + +import Fcf.Core + +-- $reexport +-- Reexported from . + +-- | Qualified name of a type family or type synonym. +data Name = MkName + Symbol -- ^ Package name + Symbol -- ^ Module name + Symbol -- ^ Type name + +-- | A general defunctionalization symbol for promoted type families. +-- It encodes saturated applications of type families. +-- +-- The second argument (@proxy :: 'ParamsProxy' name ks@) is a gadget +-- carrying implicit parameters (if any). When invoking 'Family', it must be applied to +-- a @proxy@ that corresponds to its number of implicit parameters: +-- 'P0', 'P1', 'P2', ..., 'P7', or a unary encoding using 'P0' and 'PS' for larger implicit arities. +-- (This really matters for arity 2 and more.) +-- +-- === __Implementation note__ +-- +-- This module makes heavy use of dependently typed type families. +-- There is +-- which severely limits the usability of such families when done naively. +-- +-- The workaround used here is to make the type families themselves "untyped", +-- and wrap them within "typed" synonyms. +-- +-- Making the families untyped makes GHC more lenient so that it accepts them. +-- Making the wrappers typed recovers the type inference behavior of the original family. +-- For instance, when using 'Data.Type.Bool.If', one would expect to unify +-- the types of its two branches. That is the case when constructing its +-- defunctionalization symbol using 'Family' and not with 'Family_'. +type Family :: forall (name :: Name) -> forall (ks :: Params name). ParamsProxy name ks -> forall (args :: Args name ks) -> Exp (Res name ks args) +type Family name proxy args = Family_ name proxy args + +-- | Non-dependently typed family. +type NDFamily :: forall (name :: Name) -> forall (ks :: Params name). ParamsProxy name ks -> Args name ks -> Exp (Res name ks Any) +type NDFamily name proxy = NDFamily_ name proxy Refl + +-- | Untyped internals of 'NDFamily'. +data NDFamily_ :: forall (name :: Name) -> forall (ks :: Params name). ParamsProxy name ks -> Res name ks Any :~: r -> Args name ks -> Exp r +type instance Eval (NDFamily_ name proxy e args) = Transp e (Eval (Coerce (Family name proxy args))) + +-- | Untyped internals of 'Family' +data Family_ :: Name -> Proxy ks -> args -> Exp res + +-- $arity +-- Parameters should be collected in a heterogeneous list made of @()@ and @(,)@. +-- +-- - 0: @()@ +-- - 1: @(a, ())@ +-- - 2: @(a, (b, ()))@ +-- - 3: @(a, (b, (c, ())))@ +-- - etc. + +-- | Type of implicit parameters of the named family. +type family Params (name :: Name) :: Type + +-- | Type of explicit parameters of the named family. +type Args (name :: Name) (ks :: Params name) = Args_ name ks + +-- | Untyped internals of 'Args' +type family Args_ (name :: Name) (ks :: ksT) :: Type + +-- | Type of result of the named family. +type Res (name :: Name) (ks :: Params name) (args :: Args name ks) = Res_ name ks args + +-- | Untyped internals of 'Res' +type family Res_ (name :: Name) (ks :: ksT) (args :: argsT) :: Type + +-- * Implicit parameters + +-- $tuples +-- We want implicit parameters of polykinded type families to remain implicit +-- in their promotion. +-- +-- In 'Family', the parameters are collected in a tuple. To help type inference +-- when using a promoted type family, we instantiate the spine of the tuple +-- using the following proxies. + +-- | Synonym to make explicit the dependency of the type of the +-- implicit parameters @ks@ on the @name@ of the family. +type ParamsProxy (name :: Name) (ks :: Params name) = Proxy ks + +type P0 = ('Proxy :: Proxy '()) +type P1 = PS P0 +type P2 = PS P1 +type P3 = PS P2 +type P4 = PS P3 +type P5 = PS P4 +type P6 = PS P5 +type P7 = PS P6 + +type PS (p :: Proxy ks) = ('Proxy :: Proxy '(k, ks)) + +-- * Coercions + +-- $hack These coercions are part of hacks to work around some limitations in GHC. + +-- | Sometimes GHC doesn't see that two type-level values are equal when they +-- ought to be equal. 'Coerce' lets us postpone the check to another day. +type Coerce :: forall k l. k -> l +type family Coerce (a :: k) :: l where + Coerce x = x + +-- | 'Coerce' with explicit codomain. +type CoerceTo l (a :: k) = (Coerce a :: l) + +-- | 'Coerce' with explicit domain. +type CoerceFrom k (a :: k) = Coerce a + +-- | Transport: coercion along an equality. +type Transp :: forall k l. k :~: l -> k -> l +type family Transp (e :: k :~: l) (x :: k) :: l where + Transp (_ :: k :~: k) x = x diff --git a/src/Fcf/Family/Meta.hs b/src/Fcf/Family/Meta.hs new file mode 100644 --- /dev/null +++ b/src/Fcf/Family/Meta.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE DataKinds, PolyKinds, TemplateHaskell, TypeFamilies #-} +-- {-# OPTIONS_GHC -ddump-splices #-} + +-- | 'Eval' and friends as part of the family of families. +module Fcf.Family.Meta () where + +import Fcf.Family +import Fcf.Family.TH (fcfify) + +fcfify ''Eval +fcfify ''Params +-- fcfify ''Args +-- fcfify ''Res diff --git a/src/Fcf/Family/TH.hs b/src/Fcf/Family/TH.hs new file mode 100644 --- /dev/null +++ b/src/Fcf/Family/TH.hs @@ -0,0 +1,279 @@ +{-# LANGUAGE + CPP, + ConstraintKinds, + ImplicitParams, + TemplateHaskell #-} + +-- | Template Haskell script to promote a type family to first class. +module Fcf.Family.TH + ( -- * Generate boilerplate + fcfify + + -- * Using promoted families + , promoteFamily + , promoteNDFamily + , familyName + , applyFamily + , consTuple + , paramsProxy + + -- * Predicates + , isTypeFamily + , isTypeSynonym + , isTypeFamilyOrSynonym + ) where + +import Control.Applicative (liftA2) +import Data.Function (on) +import Data.List (sort) +import Data.Maybe (fromMaybe) +import Data.Foldable (foldl') +import Data.Traversable (for) +import qualified Data.Set as Set +import Language.Haskell.TH + +import Fcf.Core +import Fcf.Family hiding (Name) + +-- | Generate the boilerplate needed to promote a type family to first class. +-- +-- See "Fcf.Family" for details on the encoding. +fcfify :: Name -> Q [Dec] +fcfify name = reifyTyInfo name >>= fcfifyInfo + where + ?funName = "fcfify" + ?name = name + +-- | Get the quoted fcf 'Fcf.Core.Family.Name' of an existing type family. +familyName :: Name -> Type +familyName name = PromotedT 'MkName + `AppT` lit (fromMaybe "" (namePackage name)) + `AppT` lit (fromMaybe "" (nameModule name)) + `AppT` lit (nameBase name) + where lit = LitT . StrTyLit + +-- | Promote a fcfified family, returning its partially applied 'Family' and +-- its arity. The result can be applied to a 'consTuple' of the appropriate size, +promoteFamily :: Name -> Q (Type, Int) +promoteFamily = promoteFamily_ ''Family + +-- | Promote a fcfified family, returning its partially applied 'Family' and +-- its arity. The result can be applied to a 'consTuple' of the appropriate size, +promoteNDFamily :: Name -> Q (Type, Int) +promoteNDFamily = promoteFamily_ ''NDFamily + +promoteFamily_ :: Name -> Name -> Q (Type, Int) +promoteFamily_ _Family name = do + info <- reifyTyInfo name + let arity = length (tiArgs info) + pure (ConT _Family `AppT` tiNameT info `AppT` paramsProxy' info, arity) + where + ?funName = "promoteFamily_" + +-- | Apply a promoted family. +-- +-- If there are more arguments than the arity of the family (as returned by 'promoteFamily'), +-- they are split and applied properly: +-- the family's main arguments are collected in a 'consTuple' and +-- the rest are applied with 'AppT'. +-- +-- If there are fewer arguments than the arity, the result is nonsense. +applyFamily :: Name -> [Q Type] -> Q Type +applyFamily name argsQ = do + (fam, arity) <- promoteFamily name + (args1, args2) <- splitAt arity <$> sequenceA argsQ + pure (fam `AppT` consTuple args1 `appsT` args2) + +paramsProxy :: Name -> Q Type +paramsProxy name = paramsProxy' <$> reifyTyInfo name + where + ?funName = "paramsProxy" + +paramsProxy' :: TyInfo -> Type +paramsProxy' info = go (length (tiParams info)) + where + go 0 = ConT ''P0 + go n = ConT ''PS `AppT` go (n-1) + +reifyTyInfo :: (?funName :: String) => Name -> Q TyInfo +reifyTyInfo name = do + let ?name = name + info <- reify name + case info of + FamilyI dec _ -> reifyTyInfoDec dec + TyConI dec -> reifyTyInfoDec dec + _ -> errorNotType + +-- | 'True' if it is a type family (open or closed). +isTypeFamily :: Name -> Q Bool +isTypeFamily name = isTypeFamilyInfo <$> reify name + +-- | 'True' if it is a type synonym. +isTypeSynonym :: Name -> Q Bool +isTypeSynonym name = isTypeSynonymInfo <$> reify name + +-- | 'True' if it is a type family or synonym. +isTypeFamilyOrSynonym :: Name -> Q Bool +isTypeFamilyOrSynonym name = liftA2 (||) isTypeFamilyInfo isTypeSynonymInfo <$> reify name + +isTypeFamilyInfo :: Info -> Bool +isTypeFamilyInfo (FamilyI (OpenTypeFamilyD _) _) = True +isTypeFamilyInfo (FamilyI (ClosedTypeFamilyD _ _) _) = True +isTypeFamilyInfo _ = False + +isTypeSynonymInfo :: Info -> Bool +isTypeSynonymInfo (TyConI (TySynD _ _ _)) = True +isTypeSynonymInfo _ = False + +-- + +type ErrCtxt = (?funName :: String, ?name :: Name) + +errorNotType :: ErrCtxt => Q a +errorNotType = fail (?funName ++ ": unexpected name, " ++ show ?name ++ " is not a type family or type synonym.") + +-- Example: +-- +-- @ +-- -- Input +-- type F a b c = (...) +-- +-- -- Output +-- type instance Params F +-- @ + +reifyTyInfoDec :: ErrCtxt => Dec -> Q TyInfo +reifyTyInfoDec (TySynD name args _) = mkInfoHead name args StarT -- TODO: don't assume result kind is Type +reifyTyInfoDec (OpenTypeFamilyD t) = reifyTyInfoTFH t +reifyTyInfoDec (ClosedTypeFamilyD t _) = reifyTyInfoTFH t +reifyTyInfoDec _ = errorNotType + +reifyTyInfoTFH :: ErrCtxt => TypeFamilyHead -> Q TyInfo +reifyTyInfoTFH (TypeFamilyHead name args resSig _) = do + res <- getRes resSig + mkInfoHead name args res + +getRes :: ErrCtxt => FamilyResultSig -> Q Type +getRes NoSig = fail (?funName ++ ": implicit result type not supported") +getRes (KindSig k) = pure k +getRes (TyVarSig (KindedTV _ _ k)) = pure k +getRes (TyVarSig PlainTV{}) = fail (?funName ++ ": implicit result type not supported") + +-- + +mkInfoHead :: Name -> [TyVarBndr ()] -> Type -> Q TyInfo +mkInfoHead name args res = do + args' <- for args (\arg -> case arg of + PlainTV _ _ -> fail "unexpected unnanotated arguments" -- as far as I understand, the binders given by reify are always annotated so this shouldn't happen + KindedTV v _ k -> pure (v, k)) + let params = collectParams args' res + pure (mkTyInfo name params args' res) + +collectParams :: [(Name, Type)] -> Type -> [Name] +collectParams args res = collect Set.empty args where + + collect bound [] = snd (addVars bound [] (getVars res)) -- collect parameters from the result type + collect bound ((v, k) : vs) = + let (bound', ws) = addVars bound [] (getVars k) in + ws ++ collect (Set.insert v bound') vs + + addVars bound ws [] = (bound, reverse ws) + addVars bound ws (x : xs) + | Set.member x bound = addVars bound ws xs + | otherwise = addVars (Set.insert x bound) (x : ws) xs + +data TyInfo = TyInfo + { tiName :: Name + , tiNameT :: Type -- ^ Encoding of name as a 'Name' + , tiParams :: [Name] + , tiParamsT :: Type -- ^ Params as a tuple + , tiArgs :: [(Name, Type)] + , tiArgsT :: Type + , tiRes :: Type + } + +appsT :: Type -> [Type] -> Type +appsT = foldl' AppT + +mkTyInfo :: Name -> [Name] -> [(Name, Type)] -> Type -> TyInfo +mkTyInfo name params args res = TyInfo + { tiName = name + , tiNameT = familyName name + , tiParams = params + , tiParamsT = consTuple (VarT <$> params) + , tiArgs = args + , tiArgsT = consTuple (uncurry (SigT . VarT) <$> args) + , tiRes = res + } + +-- | Construct a tuple suitable for a 'Family' argument. +consTuple :: [Type] -> Type +consTuple = consTuple_ (PromotedTupleT 2) (PromotedTupleT 0) + +consTupleT :: [Type] -> Type +consTupleT = consTuple_ (TupleT 2) (TupleT 0) + +consTuple_ :: Type -> Type -> [Type] -> Type +consTuple_ _ unit [] = unit +consTuple_ tup unit (t : ts) = tup `AppT` t `AppT` consTuple_ tup unit ts + +-- + +fcfifyInfo :: ErrCtxt => TyInfo -> Q [Dec] +fcfifyInfo info = do + paramsD <- declareParams info + argsD <- declareArgs info + resD <- declareRes info + familyD <- declareFamily info + pure [paramsD, argsD, resD, familyD] + +getVars :: Type -> [Name] +getVars (VarT v) = [v] +getVars (AppT t t') = getVars t ++ getVars t' +getVars (AppKindT t t') = getVars t ++ getVars t' +getVars (SigT t k) = getVars t ++ getVars k +getVars (InfixT t _ t') = getVars t ++ getVars t' +getVars (UInfixT t _ t') = getVars t ++ getVars t' +getVars (ParensT t) = getVars t +#if MIN_VERSION_template_haskell(2,19,0) +getVars (PromotedInfixT t _ t') = getVars t ++ getVars t' +getVars (PromotedUInfixT t _ t') = getVars t ++ getVars t' +#endif +getVars _ = [] + +declareParams :: TyInfo -> Q Dec +declareParams info = do + let nParams = length (tiParams info) + pure (TySynInstD (TySynEqn Nothing (ConT ''Params `AppT` tiNameT info) (consTupleT (replicate nParams StarT)))) -- TODO: don't guess Type for all params + +declareArgs :: TyInfo -> Q Dec +declareArgs info = do + pure (TySynInstD (TySynEqn Nothing + (ConT ''Args_ `AppT` tiNameT info `AppT` tiParamsT info) + (consTupleT (snd <$> tiArgs info)))) + +declareRes :: TyInfo -> Q Dec +declareRes info = do + pure (TySynInstD (TySynEqn Nothing + (ConT ''Res_ `AppT` tiNameT info `AppT` tiParamsT info `AppT` if isDT info then tiArgsT info else WildCardT) + (tiRes info))) + +isDT :: TyInfo -> Bool +isDT info = not (null (intersection (fst <$> tiArgs info) (getVars (tiRes info)))) + +intersection :: Ord a => [a] -> [a] -> [a] +intersection = intersectionSorted `on` sort + +intersectionSorted :: Ord a => [a] -> [a] -> [a] +intersectionSorted [] _ = [] +intersectionSorted _ [] = [] +intersectionSorted xxs@(x : xs) yys@(y : ys) = case compare x y of + EQ -> x : intersectionSorted xs ys + LT -> intersectionSorted xs yys + GT -> intersectionSorted xxs ys + +declareFamily :: TyInfo -> Q Dec +declareFamily info = do + pure (TySynInstD (TySynEqn Nothing + (ConT ''Eval `AppT` (ConT ''Family_ `AppT` tiNameT info `AppT` SigT WildCardT (WildCardT `AppT` tiParamsT info) `AppT` tiArgsT info)) + (foldl' AppT (ConT (tiName info)) (VarT . fst <$> tiArgs info)))) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE AllowAmbiguousTypes, DataKinds, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators #-} +-- {-# OPTIONS_GHC -ddump-splices #-} + +module Main where + +import Data.Type.Bool +import GHC.TypeNats + +import Fcf.Core +import Fcf.Family +import Fcf.Family.TH + +fcfify ''(||) +fcfify ''(+) +fcfify ''If + +type family Fst (xs :: (k, l)) :: k where Fst '(x, _) = x +type family Snd (xs :: (k, l)) :: l where Snd '(_, y) = y + +fcfify ''Fst +fcfify ''Snd + +type (:+:) = MkName "base" "GHC.TypeNats" "+" +type If_ = MkName "base" "Data.Type.Bool" "If" + +equals :: forall a b. (a ~ b) => IO () +equals = pure () + +main :: IO () +main = do + equate @(Eval (Family (:+:) P0 '(1, '(2, '())))) @3 + equate @(Eval (Family If_ P1 '( 'True , '(1, '(2, '()))))) @1 + equate @(Eval (Family If_ P1 '( 'False, '(1, '(2, '()))))) @2 + + -- Test applyFamily + equals @(Eval $(applyFamily ''(+) [ [t|3|] , [t|4|] ])) @7 + equals @(Eval $(applyFamily ''If [ [t|'True|] , [t|Int|] , [t|()|] ])) @Int + + -- Test kind inference: the two Any under If should have the same type. + equate @(Eval (Family If_ P1 '( 'True, '(Any, '(Any, '()))))) @Any + + -- The following should fail because Family_ is untyped (unlike Family) + -- equate @(Eval (Family_ If_ P1 '( 'True, '(Any, '(Any, '()))))) @Any + +-- Utils + +type family Any :: k where {} + +equate :: forall a b. (a ~ b) => IO () +equate = pure ()