summaryrefslogtreecommitdiff
path: root/doc/todo/type_level_OS_requirements
diff options
context:
space:
mode:
authorJoey Hess2016-03-08 04:24:01 -0400
committerJoey Hess2016-03-08 04:24:01 -0400
commit1311391cbf2d978d07bae679ae806e25f3388d92 (patch)
tree871a56220f3fb3e375fad2261f628dc868c8ea0d /doc/todo/type_level_OS_requirements
parent5a8ee7ea117b94222c1b3fe6d30000916755a600 (diff)
thought
Diffstat (limited to 'doc/todo/type_level_OS_requirements')
-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
+ ...
+"""]]