summaryrefslogtreecommitdiff
path: root/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
blob: 4d8cf06e367de1505b26d57be9580e0b2130a511 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
[[!comment format=mdwn
 username="joey"
 subject="""comment 1"""
 date="2016-03-08T07:31:51Z"
 content="""
ensureProperty presents a problem. Its type would become something like
this:

	ensureProperty :: Property NoInfo [OS] -> Propellor Result

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:

	foo :: Property NoInfo [Debian]
	foo = property "foo" [Debian] $ do
		os <- getOSList
		ensureProperty os (Pkg.install "bar" :: Property NoInfo [FreeBSD])
		-- type error; FreeBSD not in [Debian]

Where getOSList would pull the [Debian] out of Propellor monad
state. (Of course, ensureProperty could run getReifiedOSList itself,
`os` is only passed explicitly for illustration.)

This would need `property` to lift its [OS] parameter to a type-level
list for the resulting `Property`. How?

As for ensureProperty, something like this could work for the
implementation, if I understand reify right:

	ensureProperty :: [OS] -> Property Noinfo -> Propellor Result
	ensureProperty outeros p@(Property NoInfo inneros)
		| checkUnification (reify inneros) (reify outeros) = do
			...
		| otherwise = error "type checker should never let this be reached"
	
	checkUnification
		:: (Reifies s1 t1, Reifies s2 t2, TypesUnify t1 t2)
		=> proxy1 s1
		-> proxy2 s2
		-> Bool
	checkUnification _ _ = True -- all done at type level

	type family TypesUnify t1 t2
	...
"""]]