Polymorphic Data.Dynamic

[vivian]

At some point in the compilation process an expression acquires a fully-specified, possibly polymorphic, type. If we add an operation that join that type and that expresssion, say TypedAny, then we can implement the part of #4316 requested by mitar.

In GHCi we can evaluate HValues and also string them together with bind statements.

The function

applyDynamic :: TypedAny -> TypedAny -> Maybe TypedAny

includes in its implementation a dictionary lookup and possible dynamic object linking for class methods.

the function

fromDynamic :: TypedAny -> Maybe a

like applyDynamic, runs the typechecker at runtime to unify (and possibly link) the dynamic type (TypedAny) and the static type (a).

Conjecture Since we already have typecase (classes), with type families, this feature provides/simulates dependent types.

[vivian]

In reality those functions should probably be in a type-environment monad.

applyDynamic :: Dynamic -> Dynamic -> TypeEnv (Maybe Dynamic)
fromDynamic  :: Dynamic -> TypeEnv (Maybe a)

[vivian]

(In #4316) Now that this ticket is back to mitar's original request. I think that this feature request could be implemented (creating a meta-interpreter) on the back of #4459.

By introducing bind at the interpreter level we can invoke side-effects on a line-by-line basis within any monad construct.

[vivian]

I currently can load a module and bind the TyThing and HValue of a top-level entity

data DynamicHValue = DynamicHValue TyThing HValue

When I want to apply a DynamicHValue to another DynamicHValue (an App operation)

* I can figure out the resulting type using mkAppTy but that takes Types not TyThings. What is the correct way of getting a Type from a TyThing?

* I want to apply one HValue to another. What is the correct approach?

The second item is not so straight-forward, because the applied HValue might cause the resultant type to be less generic. A class instance might specialise the function type, in which case the linker has to link the appropriate instance.

[vivian]

Replying to vivian:

* I can figure out the resulting type using mkAppTy but that takes Types not TyThings. What is the correct way of getting a Type from a TyThing?

After some perusal, I have found mkTyVarTy, mkTyConTy, and so on which can be used to turn TyThings into Types. Is this the correct way?

[simonmar]

I'm completely confused about what this ticket is asking for. Could somebody explain in more detail please? e.g. the ticket seems to be asking for something in the Data.Dynamic library, but then there's lots of talk about something in the GHC API. What is TypedAny?

[vivian]

Replying to simonmar:

I'm completely confused about what this ticket is asking for. Could somebody explain in more detail please? e.g. the ticket seems to be asking for something in the Data.Dynamic library, but then there's lots of talk about something in the GHC API. What is TypedAny?

This ticket is about adding support for polymorphic dynamic types, which would appear in Data.Dynamic or similar as a package, so that, for example, a variable sort :: Ord a => [a] -> [a] can be loaded at runtime (like System.Plugins) and then dynamically linked/typechecked against the variable to which it is applied. Currently dynamics and plugins are limited by the monomorphic restriction.

TypedAny (renamed to DynamicHValue) is supposed to be an opaque type that wraps an HValue and a Type via the GHC API. [I have got this far, i.e. dynamically loaded code via GHC]

[In an early incarnation I was able to apply a dynamically loaded ad hoc polymorphic function to a list and print the result]

I listed this as a feature request against the GHC API because there need to be some additions 'under the hood' for this to work:

1) a way of getting the type of an expression to the value level

ty <- GHC.modInfoLookupName <-- okay for dynamically loaded code but not normal code

2) a way of getting a 'type as value' to become the type of an expression

(unsafeCoerce hvalue) :: ty <-- currently completely impossible

[simonmar]

Have you looked at polymorphic dynamics in Clean? See e.g.  http://portal.acm.org/citation.cfm?id=1863505.

[vivian]

Replying to simonmar:

Have you looked at polymorphic dynamics in Clean? See e.g.  http://portal.acm.org/citation.cfm?id=1863505.

Thanks for the reference. I've looked at the slides and now have a couple of their papers. My thinking about the issue is quite similar to one of their solutions.

[vivian]

spin    ::          [a] -> [a]
spinOrd :: Ord a => [a] -> [a]
alist   :: [Int]

So far I am able to dynamically load spin and alist and successfully print the result of the application of the parametrically polymorphic function spin to alist.

The problem (as pointed out in the reference given by simonmar above) is ad-hoc polymorphism (spinOrd).

1) How is the class information stored in an interface file?

2) How does the linker normally go about finding the correct instance of an overloaded function such as <?

If I have the Type of both spinOrd and alist then I can us mkAppyTy to unify the two types and there will be a substitution [Int/a](Ord a => [a] -> [a]) --> Ord Int => [Int] -> [Int] that tells me to use the Ord Int dictionary. I need to somehow use this information to 'specialise' the spinOrd function with methods from the Ord Int dictionary before the function is applied to the argument, which is done by the dynamic linker.

[simonpj]

I too am very hazy about what this ticket is asking for. The existing Data.Dynamic looks like this

data Dynamic = Dynamic TypeRep Obj   -- Obj is like HValue; GHC is inconsistent
toDyn :: Typeable a => a -> Dynamic
fromDynamic :: Typeable a => Dynamic -> Maybe a
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic

I think that Dynamic is what you call TypedAny.

In the existing setup you cannot put a polymorphic value in a Dynamic. So if sort :: Ord a => [a] -> [a], you can say

    toDyn (sort :: [Int] -> [Int])
    toDyn (sort :: [Bool] -> [Bool])

but if you say

    toDyn (sort :: forall a. [a] -> [a])

you'll get an ambiguity error. I think this polymorphism issue is what you are trying to solve.

I don't think it's easy:

• A Dynamic contains a TypeRep, so you'd need to elaborate TypeRep to represent polymorphic types.

• You'd need to have an instance

    instance Typable (forall a. ty) where ..
  

  and I don't know how to do that.

• When unwrapping an overloaded polymorphic value at runtime, you'd need to build a suitable dictionary to apply it to. This is no easy matter: you might need the dictionary for (Ord (Tree [Maybe Int])), say. That is, you need to invoke the full type-constraint solver, in the correct type environment.

If you wanted to solve the latter problem, I think you could get close like this

• Construct the HsSyn syntax tree for

  \(x :: forall a. Ord a => [a] -> [a]) -> (x :: [ty] -> [ty]
  

  where ty is the type you want to instantiate sort at.
• Use GHCi to typecheck and compile this
• Apply it to the polymorphic sort. That will give you a sort of type [ty] -> [ty].

Before embarking on such a project I think it would be good to learn from the Clean experience, try out their system, and (especially) articulate use cases. So that you know exactly what it is that you want to build. Perhaps start a fresh wiki page articulating (a) the motivation (b) use cases (c) the design as seen by the programmer.

Simon

[vivian]

Replying to simonpj:

I think this polymorphism issue is what you are trying to solve.

Exactly.

I don't think it's easy: * A Dynamic contains a TypeRep, so you'd need to elaborate TypeRep to represent polymorphic types.

I don't think it is easy either. I was thinking of using the Type data type which is what GHC/GHCi use.

* When unwrapping an overloaded polymorphic value at runtime, you'd need to build a suitable dictionary to apply it to. This is no easy matter: you might need the dictionary for (Ord (Tree [Maybe Int])), say. That is, you need to invoke the full type-constraint solver, in the correct type environment.

Yes, which is using the type-checker at run-time, correct?

Before embarking on such a project I think it would be good to learn from the Clean experience, try out their system, and (especially) articulate use cases. So that you know exactly what it is that you want to build. Perhaps start a fresh wiki page articulating (a) the motivation (b) use cases (c) the design as seen by the programmer.

Good idea. I've got a couple of papers about ad-hoc polymorphic dynamic types in Clean. I'll follow your suggestion about looking at Clean and also creating a wiki page.

[vivian]

New wiki page  http://hackage.haskell.org/trac/ghc/wiki/PolymorphicDynamic

[vivian]

Replying to simonpj:

* When unwrapping an overloaded polymorphic value at runtime, you'd need to build a suitable dictionary to apply it to. This is no easy matter: you might need the dictionary for (Ord (Tree [Maybe Int])), say. That is, you need to invoke the full type-constraint solver, in the correct type environment. If you wanted to solve the latter problem, I think you could get close like this * Construct the HsSyn syntax tree for {{{ \(x :: forall a. Ord a => [a] -> [a]) -> (x :: [ty] -> [ty] }}} where ty is the type you want to instantiate sort at. * Use GHCi to typecheck and compile this * Apply it to the polymorphic sort. That will give you a sort of type [ty] -> [ty].

Am I correct in reading this as an adaptor function that is applied to the ad-hoc polymorphic function to render it into the correct monomorphic instance at application site?

Do dictionaries get passed as arguments to ad-hoc polymorphic functions?

Where is the best place in the code base for me to figure out how GHC implements dictionary-passing?

Also, I'm pretty sure there needs to be a new primitive, say typeOf that, after type-checking, takes the type of an expression and lowers it to a value to be wrapped in the Dynamic datatype. Where is the best place to do that?

[vivian]

Replying to simonpj:

\(x :: forall a. Ord a => [a] -> [a]) -> (x :: [ty] -> [ty]

where ty is the type you want to instantiate sort at.

• Use GHCi to typecheck and compile this
• Apply it to the polymorphic sort. That will give you a sort of type [ty] -> [ty].

in implementing the dynApply function, the first value should be a function value. I am able to take the types of the two arguments and possibly extract a substitution. For the above example, the substitution would be [ty/a]. This substitution gives me the information that the Ord a class should be turned into the Ord ty dictionary. Which is where the above point from Simon PJ comes.

I need to conjure up an Ord Int dictionary to be able to pass it as the first argument to the HValue with type forall a.Ord a => [a] -> [a]. I can't see how to do that with the HsSyn AST since dictionaries aren't part of Haskell syntax.

Also, there needs to be a new primitive typeOf :: a -> Type that takes an expression and lowers its type to the value level in order to be able to implement toDynamic and fromDynamic. It can't be applied until after the type-checking phase.

[vivian]

Is it possible to implement the definition of a new typeOf as a Core pass? We need to wait until after the typechecking phase since until that point we may not have a type annotated to the expression.

[vivian]

Replying to simonpj:

* When unwrapping an overloaded polymorphic value at runtime, you'd need to build a suitable dictionary to apply it to. This is no easy matter: you might need the dictionary for (Ord (Tree [Maybe Int])), say. That is, you need to invoke the full type-constraint solver, in the correct type environment.

If you wanted to solve the latter problem, I think you could get close like this

• Construct the HsSyn syntax tree for

  \(x :: forall a. Ord a => [a] -> [a]) -> (x :: [ty] -> [ty]
  

  where ty is the type you want to instantiate sort at.
• Use GHCi to typecheck and compile this
• Apply it to the polymorphic sort. That will give you a sort of type [ty] -> [ty].

e.g.

t  :: Ord a => [a] -> [a]
st :: [Int] -> [Int]

I can construct the abstract syntax tree as suggested, however, I do not know

• how to correctly generate a binding/bound variable pair
• how to generate the dictionary.

Here is the HsExpr? for the function

(Ord a => [a] -> [a]) -> ([Int] -> [Int])

      let adaptor = GHC.HsLam 
                   (GHC.MatchGroup 
                    [GHC.noLoc $ GHC.Match 
                     [GHC.noLoc $ GHC.VarPat id] Nothing 
                     (GHC.GRHSs [GHC.noLoc $ GHC.GRHS [] $ 
                                    GHC.noLoc $ 
                                 (GHC.HsApp (GHC.noLoc $ GHC.HsVar id) 
                                     the_dictionary)] 
                      GHC.EmptyLocalBinds)] (mkFunTy t st))

I.e. how do I generate id and the_dictionary?

[simonpj]

The way to generate dictionaries is to call the type checker. As described in the Commentary  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/HscMain, and  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler, the type checker takes a (HsExpr Name), with no HsWrap constructors, and returns an (HsExpr Id), replete with HsWrap constructors that do the dictionary application.

It's hard to explain in a few lines! Have you read the Commentary?

[vivian]

Replying to simonpj:

It's hard to explain in a few lines! Have you read the Commentary?

I have not read all of the Commentary. I thought I was out of luck with this stub:  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Rts/Interpreter

[vivian]

Replying to simonpj:

The way to generate dictionaries is to call the type checker. As described in the Commentary  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/HscMain, and  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler, the type checker takes a (HsExpr Name), with no HsWrap constructors, and returns an (HsExpr Id), replete with HsWrap constructors that do the dictionary application.

This paragraph is from  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeChecker. The functions referred to, including sourceTypeRep are maybe part of the old typechecker?

Of particular interest are the variants SourceTy? and NoteTy? of TypeRep?.Type. The constructor SourceTy? :: SourceType? -> Type represents a type constraint; that is, a predicate over types represented by a dictionary. The type checker treats a SourceTy? as opaque, but during the translation to core it will be expanded into its concrete representation (i.e., a dictionary type) by the function [[GhcModule?(compiler/types/Type.lhs])).sourceTypeRep. Note that newtypes are not covered by SourceTypes? anymore, even if some comments in GHC still suggest this. Instead, all newtype applications are initially represented as a NewTcApp?, until they are eliminated by calls to [[GhcModule?(compiler/types/Type.lhs])).newTypeRep.

[simonpj]

Yes the "source-type" stuff is old terminology. It's called PredTy now; see the TypeRep module which has lots of comments. I've updated the Commentary.

[vivian]

Replying to vivian:

Replying to simonpj:

The way to generate dictionaries is to call the type checker. As described in the Commentary  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/HscMain, and  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler, the type checker takes a (HsExpr Name), with no HsWrap constructors, and returns an (HsExpr Id), replete with HsWrap constructors that do the dictionary application.

Is

tcRnStmt :: HscEnv -> InteractiveContext 
            -> LStmt RdrName -> IO (Messages, Maybe ([Id], LHsExpr Id))

the correct function to use? It takes RdrName but you say the type-checker takes Names. I already have Names for the class type and when attempting to use an RdrName based expression I get an error that, e.g. Ord is not in scope.

Also, is it possible to use essentially a PredType as the argument of an application?

[simonpj]

Well tcRnStmt does both renaming and typechecking. I'm not sure we curently expose a function that does just typechecking, but I'm sure it'd be possible to do so if it was useful. You could just look at the code for tcRnStmt and delete the renaming part.

In general, yes PredTypes can be arguments, certainly in Core, but without knowing a lot more it's hard to say in general.

Maybe we should move this thread to ghc-users? You are programming with the GHC API, which is great, but it's not now about changing GHC itself I think.