How to specify the type for this function?

Learn
1

Hello all,

I have a question which I hope has a simple answer and will not embarass me too much. When working with functions like this one:

clockPeriod :: forall dom period. (KnownDomain dom, DomainPeriod dom ~ period) => SNat period
(taken from Clash, Clash.Signal)

Its return value depends upon the dom type, but dom is not actually a type parameter. Assuming I have multiple doms in scope, when calling this function, how can I specify which dom I want used?

And does it have a name, a function that has a bound on a type that is not a type parameter?

2

dom is a type parameter of clockPeriod; it just doesn’t appear in the result type SNat period. (I think that’s what you mean to say?)

You can use type applications to specify specific type arguments for parameterized functions like clockPeriod: clockPeriod @YourDomType is what that would look like. You can see a few examples of this nearby in the Clash documentation.

3

Let’s do the easy part first: yes, that’s called a ‘phantom type’. Doesn’t appear on RHS of => is the critical part.

The modern way is Visible Type Applications, spelled @:

p = clockPeriod @MyDom

(And what @rhendric said.)

4

I don’t know Clash, but that signature looks a bit odd:

  • DomainPeriod is a type synonym:
    type DomainPeriod (dom :: Domain) = DomainConfigurationPeriod (KnownConf dom)
  • in which DomainConfigurationPeriod is a type family – so we must supply dom to it.
  • (KnownConf is another type synonym.)
  • ... ~ period (the ~) means constrain period to be the same type as LHS.
  • Then I don’t see that period is doing anything useful. Could that signature be
clockPeriod :: forall dom. (KnownDomain dom) => SNat (DomainPeriod dom)
5

dom is a type parameter of clockPeriod ; it just doesn’t appear in the result type SNat period . (I think that’s what you mean to say?)

Yes - I guess so.

You can use type applications to specify specific type arguments for parameterized functions like clockPeriod : clockPeriod @YourDomType is what that would look like. You can see a few examples of this nearby in the Clash documentation.

Great, thank you. I was building up to a second question about what those @s were, and now I’m glad at least I didn’t bundle that question into this one.

6

Aha. You mean the period here is redundant, because it’s already specified by the DomainPeriod dom type parameter? It might just be a convenience function, I’m not sure.

Thanks for giving me this crucial “Phantom Types” term.