From 4192be1917bb2751aecab9476b6cfd69fda6707f Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Tue, 8 Mar 2016 05:09:07 -0400 Subject: more thoughts --- doc/todo/type_level_OS_requirements.mdwn | 10 +++--- ...ent_1_507e3b74c2a3b8f41da5d3eddf197c6f._comment | 42 +++++++++++++++------- 2 files changed, 35 insertions(+), 17 deletions(-) (limited to 'doc/todo') 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" -- cgit v1.2.3