Currently, properties don't indicate what OS, or OS's, they work with.
Using withOS means throwing a runtime error on an unsupported OS. Yuck.
Could the OS of a property be lifted to the type level?
If we had Property i '[OS] then combining properties would need to update
the type-level OS list.
For example, Property i '[Debian, FreeBSD] combined with Property i '[Debian, Buntish]
yields a Property i '[Debian] -- the intersection of the OS's supported by
the combined properties.
And, combining two properties that demand different OS's would need to be a type error.
Another kind of property combination would be to glue two properties that support different OS's together, yielding a property that supports both, and so has both in its '[OS] type list, and that choses which to run using withOS.
The os property would need to yield a Property (os:[]), where the type
level list contains a type-level eqivilant of the value passed to the
property. Is that possible to do?
Or, alternatively, could have less polymorphic osDebian etc
properties replace the os property.
If a Host's list of properties, when all combined together,
contains more than one element in its '[OS], that could be a type error,
the OS of the Host is indeterminite. Which would be fixed by using the os
property to specify.
On the other hand, if a Host's list of properties yields a single OS
the type needs to be just Host.
After all, propellor operates on a [Host]; if we had Host OS,
the list couldn't contain host's with different OS's.
One way to do this would be to make a Host not contain a Property, but a Propellor Result. The list of Properties could be combined together, and the Propellor Result extracted from the resulting single property.
This is somewhat similar to type level port conflict detection.
Note that propellor needs to remain buildable with Debian stable's ghc 7.6.3. I was able to get the type level OS implementation backported to work with that version, with some added ugliness.
--Joey
ensureProperty presents a problem. Its type would become something like this:
So, using ensureProperty inside a Property would not make the outer Property inherit the OS requirements of the inner properties.
I don't see a way to propigate the '[OS] out to the outer Property from the Propellor monad where ensureProperty is used.
Hmm, perhaps the outer Property's '[OS] could be reified and passed into ensureProperty. Then reflect it back to a type, and require that inner Property's '[OS] contains everything in the outer '[OS] list.
I'm still vague on reifying and reflecting types, so I don't know if this can be done in a way that lets the type checker detect errors.
Something like this, maybe:
Where getOSList would pull the
debianvalue out of Propellor monad state. (Of course, ensureProperty could run getReifiedOSList itself,osis only passed explicitly for illustration.)The type of
mkpropertythus reflects the reified type passed into it. Here's a demo showing how to do that:Similary:
As for ensureProperty, something like this could work for the implementation:
I've made a typed-os-requirements branch that has type-level OS lists implemented.
For example:
What this is lacking is type-level equality for OSList. The complicated type above should be equivilant to
OSList '[OSDebian, OSFreeBSD]So, this doesn't type check yet:
Also,
intersectSupportedOSshould have an additional constraint, to prevent it from generating an empty type-level list.Asked about what I'm stuck on: http://stackoverflow.com/questions/35878018/how-to-write-an-intersection-function-for-type-level-lists
Ok, got intersectSupportedOS fixed.
So, the type level OS lists are ready, on to the next step ... eventually ...
I got it to throw a nice type error when intersection of two OS lists yields an empty list:
I think the next step would be actually adding the OSList to Property and making combining properties combine their OS lists at the type level.
I've added a prototype of
ensurePropertythat enforces at the type level that the property it runs will work on an OS that's passed to it.It was easier than I thought; I didn't turn out to need reification. Just pass in the outer OS:
At this point, I'm confident this can be rolled out into propellor; there should be no big bumps in the road ahead.
I just came across another issue where the Buntish release string made a difference. I'll open a PR tomorrow sometime to show what I did (hardcoded) and maybe we can think of something cleverer using the typesystem, too.
Thanks!
This looks to be adding a new type parameter:
Property NoInfo DebianOnlySo does type level resource conflict detection.
Would it make sense to include both targeted OS's and used resources in the same list of types? Otherwise, we end up with 4 type parameters, which is increasingly a mouthful to write:
Property NoInfo DebianOnly '[]Since most properties use no ports or other resources, combining the resources lets type alises like DebianOnly be all that needs to be specified:
Property NoInfo DebianOnlyWhen there is a resource, can use
':to add it to the list:Property NoInfo (Port 80 ': Port 443 ': DebianOnly)Seems reasonable. The implementation of combining such type lists may get complicated, because there will be different rules for target OS's vs resources.
Could also move the NoInfo|HasInfo into the type list. A list without HasInfo would be used instead of an explicit NoInfo, so:
Property (HasInfo ': DebianOnly)I'm currently using a simple sum type to describe the target OS:
This could in theory specify much more information about the OS version and architecture. Even type-level strings could be used to include release names.
But, the old version of ghc being targeted doesn't have the nice Data.Type.Equality stuff; I had to implement my own clumsily and it would quickly hit a combinatorial explosion with more data.
(There may be a better way than the way I found which works back to ghc 7.6.3.)
Of course, we can always add more detail later. Since type aliases are used,
Propety Debianwhich only specifiesOSDebiannow, could easily be changed at some point to specifyOSDebian AnyVersion AnyArch.The list of child properties is a problem, because it would need to be
[Property proptypes]and the proptypes will vary, so heterogenious list.The proptypes of the child properties needs to influence the proptypes of the parent anyway. Take intersection of the parent's targets and its children's targets, plus both's non-target types.
So, could calculate that proptypes, and use it as the type of both the parent property, and each child property in the list.