summaryrefslogtreecommitdiff
path: root/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
diff options
context:
space:
mode:
Diffstat (limited to 'doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment')
-rw-r--r--doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment57
1 files changed, 57 insertions, 0 deletions
diff --git a/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment b/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
new file mode 100644
index 00000000..4d8cf06e
--- /dev/null
+++ b/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
@@ -0,0 +1,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
+ ...
+"""]]