Q: Can type of InjectWith / InputType be generalized?

[aleator]

This is more a question than an issue. I was earlier looking at how to recover BB-encodings on the Haskell side. The general idea I had was to use Expr Src Dynamic which could hold functions inside the dynamic. Then the normalizer, when it encounters an application of Èmbed would unwrap the function from dynamic, interpret the argument value, apply the function and inject the result back.

This has two (obvious) caveats. First being that the InputType has an X where I'd want a Dynamic. Would it be acceptable to relax this?

The other, is, of course that the argument subexpression might not have a suitable normal form by itself. Would this be solved by additional normalization before computing the 'special' application?

[Gabriella439]

Sorry for the delayed response on this

So I'm not sure if we should reuse the Embed constructor for this purpose, since I would like to reserve that for import-related functionality. However, we could in principle add a new constructor for storing arbitrary Haskell functions

Also, this doesn't necessarily require using Dynamic. I believe you would need to store is an expression of type forall s a. Expr s a -> Expr s a. Then a Haskell function could be converted to that type using a helper function with a type similar to:

wrap :: (Interpret input, Inject output) => (input -> output) -> Expr s a -> Expr s a

[Profpatsch]

I’d love to have this feature as well. If we can call dhall functions from the interpreting language, we should also be able to do the other way around.

Small elaboration of my use-case:

I want to be able to have “opaque” data in my dhall code, where the interpretation/implementation is up to the interpreter, yet the dhall file still type-checks with the normal dhall tools (no custom extension of the normalizer necessary to interpret the dhall file).

For example, imagine a window manager configuration, and the user should be able to add and subtract keys from the set, but the set itself is not defined in dhall:

let KeyMap = { key : Text, command : Text }

in    λ(KeySet : Type)
	→ λ(defaultKeyMap : KeySet)
	→ λ(addKeys : KeySet → List KeyMap → KeySet)
	→ λ(removeKeys : KeySet → List Text → KeySet)
	→   addKeys
		(removeKeys defaultKeyMap [ "key1", "key2" ])
		[ { key = "Meta-x", command = "emacsclient" } ]
	  : KeySet

which type-checks and normalizes just fine in dhall and exposes some functions that the user can apply to the opaque data type. This way the Haskell implementation can decide how to represent the data structure and how to implement the interpreter for the small KeySet DSL.

It nearly works, except I cannot pass Haskell functions to dhall right now, because the Inject instance for functions Inject a -> Interpret b is missing.

If it’s possible I’d like to pair on this, because I’m interested in how to implement such a feature.

[Gabriella439]

@Profpatsch: Basically, you would need to add a new constructor to the Expr type that can store a Haskell function and its type, like this:

data Expr s a =
    ...
    | HaskellFunction { inputType :: Expr s a, outputType :: Expr s a, function :: Expr s a -> Expr s a }

... and then fix all the type errors. Then I believe you'd be able to implement the Inject instance you want.

However, even if you did have such an instance your example wouldn't work because you wouldn't be able to Inject a Type (i.e. the λ(KeySet : Type) → … in your example)

[quasicomputational]

FWIW, I've experimented locally with a Profunctor version of InputType and found it useful:

data InputType a b = InputType
  { embed :: a -> Dhall.Core.Expr Dhall.Parser.Src b
  , declared :: Dhall.Core.Expr Dhall.Parser.Src b
  }

The context is that some symbolic 'imports' are present in the output, which are resolved differently depending on format - e.g., one format's happy to have actual imports, but another wants them inlined; both of those are just a fmap away, and allow code sharing.

Specifically the current default-factoring code in CabalToDhall, and it's a lot more straightforward with the profunctor InputType. The code is almost applying the Yoneda lemma if you squint, but Expr is a perfectly good Functor so I feel like I shouldn't have to.

[Profpatsch]

However, even if you did have such an instance your example wouldn't work because you wouldn't be able to Inject a Type (i.e. the λ(KeySet : Type) → … in your example)

I solved that, by writing this module: https://github.com/openlab-aux/vuizvui/blob/master/pkgs/profpatsch/xmonad/DhallTypedInput.hs