GHC API: How to determine Type.Type equality when using type
operators?
Simon PeytonJones
simonpj at microsoft.com
Fri Jul 3 06:27:37 EDT 2009
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 toplevel typefunction 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 toplevel typefunction 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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskellusers
 bounces at haskell.org] On Behalf Of Christiaan Baaij
 Sent: 02 July 2009 11:20
 To: glasgowhaskellusers at 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 fixedsize 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 parameterizeddata package [1], except
 that we
 use typelevel integers from the tfp library [2] to define the static
 vector
 lenght. The tfp library support things like typelevel 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 typeoperator 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 typeoperator.

 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/parameterizeddata
 [2] http://hackage.haskell.org/package/tfp
 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list