summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorJoey Hess2016-03-08 05:09:10 -0400
committerJoey Hess2016-03-08 05:09:10 -0400
commitf06fbbbd6855ee6c53c9524a54c0773b350ebd87 (patch)
tree75dd1b94a837b9e81e0b425c21961d7e1a463b07 /doc
parentf40c452eadac619d6e0c62b6aac9d86255d6318e (diff)
parent4192be1917bb2751aecab9476b6cfd69fda6707f (diff)
Merge branch 'joeyconfig'
Diffstat (limited to 'doc')
-rw-r--r--doc/todo/type_level_OS_requirements.mdwn10
-rw-r--r--doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment42
2 files changed, 35 insertions, 17 deletions
diff --git a/doc/todo/type_level_OS_requirements.mdwn b/doc/todo/type_level_OS_requirements.mdwn
index 5654d49a..65e6099f 100644
--- a/doc/todo/type_level_OS_requirements.mdwn
+++ b/doc/todo/type_level_OS_requirements.mdwn
@@ -4,11 +4,11 @@ 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
+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
+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
@@ -19,7 +19,7 @@ Host?
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
+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
@@ -30,7 +30,7 @@ Or, alternatively, could have less polymorphic `debian` 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 needs to be a type error,
+contains more than one element in its '[OS], that needs to be a type error,
the OS of the Host is indeterminite. Which would be fixed by using the `os`
property to specify.
diff --git a/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment b/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
index 4d8cf06e..fa9a7eb1 100644
--- a/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
+++ b/doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment
@@ -6,42 +6,60 @@
ensureProperty presents a problem. Its type would become something like
this:
- ensureProperty :: Property NoInfo [OS] -> Propellor Result
+ 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
+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
+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.
+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
+ 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] out of Propellor monad
+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.)
-This would need `property` to lift its [OS] parameter to a type-level
-list for the resulting `Property`. How?
+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, if I understand reify right:
+implementation:
- ensureProperty :: [OS] -> Property Noinfo -> Propellor Result
+ ensureProperty :: '[OS] -> Property Noinfo -> Propellor Result
ensureProperty outeros p@(Property NoInfo inneros)
- | checkUnification (reify inneros) (reify outeros) = do
+ | (reify inneros $ \t1 -> reify outeros $ \t2 -> checkUnification t1 t2) = do
...
| otherwise = error "type checker should never let this be reached"