Converting a Constraint to Bool

Using the Constraint type and the ConstraintKinds extension, is there any way we can determine if a Constraint is satisfied (i.e. a type-level function of type Constraint -> Bool using DataKinds)? -- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

It's a bad idea. See, even if a constraint is not satisfied, there is no reason why it can't be satisfied later, in another module. So, inclusion of another module might change the behaviour of the code that was already compiled.
I'm sure that after some oleging you'd find something that is more or less similar to what you want, but it's still a bad idea.
16.10.2014, 14:58, "Ivan Lazar Miljenovic"
Using the Constraint type and the ConstraintKinds extension, is there any way we can determine if a Constraint is satisfied (i.e. a type-level function of type Constraint -> Bool using DataKinds)?
-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I recently experimented with that kinda stuff. See the following:
type family SelectPrivilege a :: Bool
type instance SelectPrivilege ReadTransaction = True
type instance SelectPrivilege WriteTransaction = True
type family UpdatePrivilege a :: Bool
type instance UpdatePrivilege ReadTransaction = False
type instance UpdatePrivilege WriteTransaction = True
data Read
data Write
data Transaction t r
executeUpdateTransaction :: UpdatePrivilege t ~ True => Transaction t r -> IO r
executeUpdateTransaction =
undefined
The above code ensures that transactions of type Transaction Read r cannot
be executed using the executeUpdateTransaction function. However then the
same type level logic can be encoded using an existence of a type class
instance:
class SelectPrivilege t
instance SelectPrivilege ReadTransaction
instance SelectPrivilege WriteTransaction
class UpdatePrivilege t
instance UpdatePrivilege WriteTransaction
data Read
data Write
data Transaction t r
executeUpdateTransaction :: UpdatePrivilege t => Transaction t r -> IO r
executeUpdateTransaction =
undefined
2014-10-16 14:58 GMT+04:00 Ivan Lazar Miljenovic
Using the Constraint type and the ConstraintKinds extension, is there any way we can determine if a Constraint is satisfied (i.e. a type-level function of type Constraint -> Bool using DataKinds)?
-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Oct 16, 2014, at 6:58 AM, Ivan Lazar Miljenovic
Using the Constraint type and the ConstraintKinds extension, is there any way we can determine if a Constraint is satisfied (i.e. a type-level function of type Constraint -> Bool using DataKinds)?
No, for precisely this reason:
On Oct 16, 2014, at 7:06 AM, Miguel Mitrofanov
See, even if a constraint is not satisfied, there is no reason why it can't be satisfied later, in another module. So, inclusion of another module might change the behaviour of the code that was already compiled.
But I disagree here:
I'm sure that after some oleging you'd find something that is more or less similar to what you want, but it's still a bad idea.
If you figure out some way to encode the feature you're after (converting a Constraint to a Bool like this), you've broken the type system. Please submit a bug report! Thanks, Richard

On 17 October 2014 05:12, Richard Eisenberg
On Oct 16, 2014, at 6:58 AM, Ivan Lazar Miljenovic
wrote: Using the Constraint type and the ConstraintKinds extension, is there any way we can determine if a Constraint is satisfied (i.e. a type-level function of type Constraint -> Bool using DataKinds)?
No, for precisely this reason:
On Oct 16, 2014, at 7:06 AM, Miguel Mitrofanov
wrote: See, even if a constraint is not satisfied, there is no reason why it can't be satisfied later, in another module. So, inclusion of another module might change the behaviour of the code that was already compiled.
Oh, because any such conversions would be done at compile time of the module that defined such behaviour and won't take into account any more instances or classes? Didn't think about that...
But I disagree here:
I'm sure that after some oleging you'd find something that is more or less similar to what you want, but it's still a bad idea.
If you figure out some way to encode the feature you're after (converting a Constraint to a Bool like this), you've broken the type system. Please submit a bug report!
Thanks, Richard
-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com
participants (4)
-
Ivan Lazar Miljenovic
-
Miguel Mitrofanov
-
Nikita Volkov
-
Richard Eisenberg