From 1311391cbf2d978d07bae679ae806e25f3388d92 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Tue, 8 Mar 2016 04:24:01 -0400 Subject: thought --- ...ent_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment | 57 ++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 doc/todo/type_level_OS_requirements/comment_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment 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 + ... +"""]] -- cgit v1.2.3