GHC API: How to determine Type.Type equality when using type operators?
Hi all, I've been doing some work with the GHC API where I translate Haskell to VHDL, and as such I have to translate Haskell Types to VHDL Types. I store the translations in a Map as such: -- A orderable equivalent of CoreSyn's Type for use as a map key newtype OrdType = OrdType { getType :: Type.Type } instance Eq OrdType where (OrdType a) == (OrdType b) = Type.tcEqType a b instance Ord OrdType where compare (OrdType a) (OrdType b) = Type.tcCmpType a b -- A map of a Core type to the corresponding type name type TypeMap = Map.Map OrdType (AST.VHDLId, Either AST.TypeDef AST.SubtypeIn) This solution work fine for 'simple' types and ensures that the VHDL Type definitions are all unique. However, a problem rises when type operators come in to play, as Type.tcEqType does not know the 'rules' of these type operators and can thus not infer that two types are equal. Let me give some context for my problem: We use statically fixed-size vectors instead of lists, as we always want to know the static length of an array. We use a vector implementation similar to Data.Param.FSVec defined in the parameterized-data package [1], except that we use type-level integers from the tfp library [2] to define the static vector lenght. The tfp library support things like type-level multiplication, something that we use in our vector library. Now, say we have two bit vectors of length 12 defined as such: a :: Vector D12 Bit b :: Vector (D3 :*: D4) Bit The GHC type checker can infer that 'a' and 'b' are of equal type, as it knows the definitions for the ':*:' multiplication type-operator that is defined in the tfp library. Of course, the only answer Type.tcEqType can give us if we ask if the types of 'a' and 'b' are equals is False, as it does not know the context provided by the type-operator. So my question is: Is there a functions in the GHC API that I can use to check the equality of two types given the context provided by certain type operators? I have looked at the Haddock documentation, the GHC Wiki, and the GHC code itself, but have been unable to find such a function. Regards, Christiaan [1] http://hackage.haskell.org/package/parameterized-data [2] http://hackage.haskell.org/package/tfp
I believe that you are asking about type functions. Specifically, I think what you are asking is this: How can I normalise a type, by rewriting it exhaustively using the top-level type-function definitions I think the function TcTyFuns.tcNormaliseFamInst (rather an odd name!) does this. But it's not very helpful to you because it's in the main typechecker monad. -- |Normalise the given type as far as possible with toplevel equalities. -- This results in a coercion witnessing the type equality, in addition to the -- normalised type. -- tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType) You probably wanted something like normaliseType :: FamInstEnv -> TcType -> (CoercionI, TcType) where FamInstEnv contains the top-level type-function definitions. I believe that the only use of the monad is to carry the definitions around, so it should be easy to define the former in terms of the latter, although that'd need a bit of refactoring. Manuel may know more Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Christiaan Baaij | Sent: 02 July 2009 11:20 | To: glasgow-haskell-users@haskell.org | Subject: GHC API: How to determine Type.Type equality when using type operators? | | Hi all, | | I've been doing some work with the GHC API where I translate Haskell | to VHDL, | and as such I have to translate Haskell Types to VHDL Types. I store the | translations in a Map as such: | | | -- A orderable equivalent of CoreSyn's Type for use as a map key | newtype OrdType = OrdType { getType :: Type.Type } | instance Eq OrdType where | (OrdType a) == (OrdType b) = Type.tcEqType a b | instance Ord OrdType where | compare (OrdType a) (OrdType b) = Type.tcCmpType a b | | -- A map of a Core type to the corresponding type name | type TypeMap = Map.Map OrdType (AST.VHDLId, Either AST.TypeDef | AST.SubtypeIn) | | | This solution work fine for 'simple' types and ensures that the VHDL | Type | definitions are all unique. However, a problem rises when type | operators come | in to play, as Type.tcEqType does not know the 'rules' of these type | operators | and can thus not infer that two types are equal. Let me give some | context for | my problem: | | We use statically fixed-size vectors instead of lists, as we always | want to | know the static length of an array. We use a vector implementation | similar to | Data.Param.FSVec defined in the parameterized-data package [1], except | that we | use type-level integers from the tfp library [2] to define the static | vector | lenght. The tfp library support things like type-level multiplication, | something that we use in our vector library. | | Now, say we have two bit vectors of length 12 defined as such: | | a :: Vector D12 Bit | b :: Vector (D3 :*: D4) Bit | | The GHC type checker can infer that 'a' and 'b' are of equal type, as | it knows | the definitions for the ':*:' multiplication type-operator that is | defined in | the tfp library. Of course, the only answer Type.tcEqType can give us | if we | ask if the types of 'a' and 'b' are equals is False, as it does not | know the | context provided by the type-operator. | | So my question is: | Is there a functions in the GHC API that I can use to check the | equality of | two types given the context provided by certain type operators? I have | looked | at the Haddock documentation, the GHC Wiki, and the GHC code itself, | but have | been unable to find such a function. | | Regards, | Christiaan | | | [1] http://hackage.haskell.org/package/parameterized-data | [2] http://hackage.haskell.org/package/tfp | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
I believe that you are asking about type functions. Specifically, I think what you are asking is this:
How can I normalise a type, by rewriting it exhaustively using the top-level type-function definitions
That is indeed a better formulation of my original question
I think the function TcTyFuns.tcNormaliseFamInst (rather an odd name!) does this. But it's not very helpful to you because it's in the main typechecker monad.
At the moment it is not such a big problem that it is in the typechecker monad, as we run some parts of our compiler in a GHC Monad, and can thus initialize a typechecker monad with the function TcRnMonad.initTc. However, at the moment I can't get to normalise the types as far as I had hoped. Here is an example of my debug output: Before normalisation: Types.Data.Num.Decimal.Literals.D4 Types.Data.Num.Ops.:*: Types.Data.Num.Decimal.Literals.D3 After normalisation: Types.Data.Num.Decimal.Digits.Dec (Types.Data.Num.Decimal.Digits.DecN Types.Data.Num.Ops.:. Types.Data.Num.Decimal.Digits.Dec4) Types.Data.Num.Ops.:*: Types.Data.Num.Decimal.Digits.Dec (Types.Data.Num.Decimal.Digits.DecN Types.Data.Num.Ops.:. Types.Data.Num.Decimal.Digits.Dec3) So, currently I can normalize the synonyms D4 and D3, but I can't normalize the type function :*:. Maybe it has something to do with how I load the module and its dependencies. Below is the code that I use to normalize a type-level integer from the tfp library, I hope it's not too much to read. normalise_tfp_int :: Type.Type -> Type.Type normalise_tfp_int ty = unsafeRunGhc $ do -- Automatically import modules for any fully qualified identifiers setDynFlag DynFlags.Opt_ImplicitImportQualified let modules = map GHC.mkModuleName ["Types.Data.Num"] nty <- normaliseType modules ty return nty normaliseType :: [Module.ModuleName] -> Type.Type -> GHC.Ghc Type.Type normaliseType modules ty = do env <- GHC.getSession nty <- HscTypes.ioMsgMaybe $ MonadUtils.liftIO $ -- Initialize the typechecker monad TcRnMonad.initTcPrintErrors env PrelNames.iNTERACTIVE $ do mapM importModule modules -- Normalize the type (_, nty) <- TcTyFuns.tcNormaliseFamInst ty return nty return nty importModule :: Module.ModuleName -> TcRnTypes.RnM () importModule mod = do let reason = Outputable.text "Hardcoded import" let pkg = Nothing -- Load the interface. iface <- LoadIface.loadSrcInterface reason mod False pkg let deps = HscTypes.mi_deps iface let orphs = HscTypes.dep_orphs deps let finsts = HscTypes.dep_finsts deps -- Load the dependencies and family instances LoadIface.loadOrphanModules orphs False LoadIface.loadOrphanModules finsts True
Christiaan Baaij:
I believe that you are asking about type functions. Specifically, I think what you are asking is this:
How can I normalise a type, by rewriting it exhaustively using the top-level type-function definitions
That is indeed a better formulation of my original question
I think the function TcTyFuns.tcNormaliseFamInst (rather an odd name!) does this. But it's not very helpful to you because it's in the main typechecker monad.
At the moment it is not such a big problem that it is in the typechecker monad, as we run some parts of our compiler in a GHC Monad, and can thus initialize a typechecker monad with the function TcRnMonad.initTc.
However, at the moment I can't get to normalise the types as far as I had hoped. Here is an example of my debug output:
Before normalisation: Types.Data.Num.Decimal.Literals.D4 Types.Data.Num.Ops.:*: Types.Data.Num.Decimal.Literals.D3
After normalisation: Types.Data.Num.Decimal.Digits.Dec (Types.Data.Num.Decimal.Digits.DecN Types.Data.Num.Ops.:. Types.Data.Num.Decimal.Digits.Dec4) Types.Data.Num.Ops.:*: Types.Data.Num.Decimal.Digits.Dec (Types.Data.Num.Decimal.Digits.DecN Types.Data.Num.Ops.:. Types.Data.Num.Decimal.Digits.Dec3)
So, currently I can normalize the synonyms D4 and D3, but I can't normalize the type function :*:. Maybe it has something to do with how I load the module and its dependencies.
Yes, it has something to do with module loading and the type-checker monad. It's not enough to load the modules, you also need to initialise those components of the type-checker monad that contain the environment of visible type instance declarations. The component is called tcg_fam_inst_env and you can see in the function TcRnDriver.tcRnImports how to extend it. You did well in remembering to load the orphan modules, but you also ought to call FamInst.checkFamInstConsistency to check for overlapping instances in the modules that you are loading (it's used right at the end of TcRnDriver.tcRnImports). Hope that helps a bit. Manuel
participants (3)
-
Christiaan Baaij -
Manuel M T Chakravarty -
Simon Peyton-Jones