summaryrefslogtreecommitdiff
path: root/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
blob: b282e61edb250fbe5d4d4853182e037ef19a0606 (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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
[[!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:

	debian :: '[Debian]
	debian = undefined

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

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

The type of `mkproperty` thus reflects the reified type passed into it.
Here's a demo showing how to do that:
	
	demo :: (Reifies s t) => proxy s -> (Bool, t)
	demo p = (True, reflect p)

	*Main> :t (reify "foo") demo
	(reify "foo") demo :: (Bool, [Char])
	*Main> :t (reify False) demo
	(reify False) demo :: (Bool, Bool)

Similary:

	mkproperty :: (Reifies s os) => proxy s -> Desc -> Propellor Result -> Property NoInfo os
	mkproperty os desc a = Property desc $ do
		setOSList (reflect os)
		a

As for ensureProperty, something like this could work for the
implementation:

	ensureProperty :: '[OS] -> Property Noinfo -> Propellor Result
	ensureProperty outeros p@(Property NoInfo inneros)
		| (reify inneros $ \t1 -> reify outeros $ \t2 -> checkUnification t1 t2) = 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
	...
"""]]