Type Families and enhanced constraints (at run-time)
Hi, I hope this is the right place to ask about working with type families...I want to make a library of Set operations that carries proofs at the type level, e.g. to make things like this possible,
insert :: Member e s' T => e -> Set s -> Set s' union :: Union s t u => Set s -> Set t -> Set u
The trouble is designing the Set datatype so it can be used in type constraints *and* in run-time functions....Something similar is of course possible with fun deps, and I knocked something up following the example of Conrad Parker's 'Instant Insanity' but, crucially, that code is 'trapped' in the type system with no populated types. I want term-level/run-time functions with enhanced constraints, such as in the example Manuel posted in haskell-cafe:
data Z data S a
data SNat n where Zero :: SNat Z Succ :: SNat n -> SNat (S n)
zero = Zero one = Succ zero
type family (:+:) n m :: * type instance Z :+: m = m type instance (S n) :+: m = S (n :+: m)
add :: SNat n -> SNat m -> SNat (n :+: m) add Zero m = m add (Succ n) m = Succ (add n m)
This seems like "the best of both worlds" -- maybe it could be a general strategy for making for making these enhanced constraints at the term-level? Make a (populated) GADT and parameterise it with a phantom type (perhaps amongst other things). Make a type operator that can be used to express the constraint on the phantom types carried around by the "regular" populated type. When the type operator appears in the codomain of the function it's a compile-time check on the implementation of that function and when in the domain it checks the user at run-time. However, (SNat n) can be put very succinctly because it doesn't need to carry a value around other than the Peano number in the phantom type. What about Sets? In my case the values in the sets are just labels and could well be empty:
data A ; data B ; data C
And I also need to express the cons-ness -- I don't think that needs fancy constraints so it can be done with terms, e.g., an underlying sequence such as in the Collects example. Generally I need to work out what needs to be run-time and what compile-time but I think that would follow from getting the combinations of types and terms in the Set abstraction right...could someone give me a pointer with this? Many thanks, Jim
Whenever you want to maintain type-level assertions of properties of you functions, you need to decide *how much* of the value-level information do you need on the type level to express and check the properties that you are interested in. My SNat example was at one extreme end of the spectrum: *complete* value-level information is reflected at the type level. In other case, it is only necessary to reflect partial information; eg, when reasoning about bounds-checks of bounded lists or arrays, only the length, but not the exact elements need to be reflected. In other words, first you need to decide what properties you want to enforce and what information you need to decide those properties. Coming back to your set example, what properties do you want to enforce/check and what information do you need to do that? In the extreme case, you could reflect the entire contents of each set at the type-level using a singleton set type (and corresponding singleton types for the set elements). However, that also would mean that all your value-level set operations will already have to be completely executed by the type checker at compile time, which is probably not what you want. Does this make sense? Manuel Jim Burton:
Hi, I hope this is the right place to ask about working with type families...I want to make a library of Set operations that carries proofs at the type level, e.g. to make things like this possible,
insert :: Member e s' T => e -> Set s -> Set s' union :: Union s t u => Set s -> Set t -> Set u
The trouble is designing the Set datatype so it can be used in type constraints *and* in run-time functions....Something similar is of course possible with fun deps, and I knocked something up following the example of Conrad Parker's 'Instant Insanity' but, crucially, that code is 'trapped' in the type system with no populated types. I want term-level/run-time functions with enhanced constraints, such as in the example Manuel posted in haskell-cafe:
data Z data S a
data SNat n where Zero :: SNat Z Succ :: SNat n -> SNat (S n)
zero = Zero one = Succ zero
type family (:+:) n m :: * type instance Z :+: m = m type instance (S n) :+: m = S (n :+: m)
add :: SNat n -> SNat m -> SNat (n :+: m) add Zero m = m add (Succ n) m = Succ (add n m)
This seems like "the best of both worlds" -- maybe it could be a general strategy for making for making these enhanced constraints at the term-level? Make a (populated) GADT and parameterise it with a phantom type (perhaps amongst other things). Make a type operator that can be used to express the constraint on the phantom types carried around by the "regular" populated type. When the type operator appears in the codomain of the function it's a compile-time check on the implementation of that function and when in the domain it checks the user at run- time.
However, (SNat n) can be put very succinctly because it doesn't need to carry a value around other than the Peano number in the phantom type. What about Sets? In my case the values in the sets are just labels and could well be empty:
data A ; data B ; data C
And I also need to express the cons-ness -- I don't think that needs fancy constraints so it can be done with terms, e.g., an underlying sequence such as in the Collects example. Generally I need to work out what needs to be run-time and what compile-time but I think that would follow from getting the combinations of types and terms in the Set abstraction right...could someone give me a pointer with this?
Many thanks,
Jim
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
On Fri, 2007-11-30 at 13:37 +1100, Manuel M T Chakravarty wrote: [...]
In other words, first you need to decide what properties you want to enforce and what information you need to decide those properties. Coming back to your set example, what properties do you want to enforce/check and what information do you need to do that? In the extreme case, you could reflect the entire contents of each set at the type-level using a singleton set type (and corresponding singleton types for the set elements). However, that also would mean that all your value-level set operations will already have to be completely executed by the type checker at compile time, which is probably not what you want.
Does this make sense?
Yes, and thanks for your reply. What I really need are both ends of the spectrum! It's reasoning with these sets that is important to me and the contents are arbitrary, so operations on them should become proof-carrying code, but they should be "constructable" at run-time. This will obviously require that two sets with different elements have different types so I thought about carrying around the extra info alongside the regular collection:
data N ; data A tail ; data B tail
data TInfo t where Nil :: TInfo N InsA :: TInfo t -> TInfo (A t) InsB :: TInfo t -> TInfo (B t)
empty = Nil a_empty = InsA empty
data Set t a = Set (TInfo t) [a]
So a value of type Set t Char might have the type "Set (TInfo (A (B N))) ['a', 'b']" and I can start creating type families to enforce constraints. But this doesn't work:
insert :: Char -> Set t Char -> Set t Char insert c (Set tinfo cs) = case c of 'A' -> Set (InsA tinfo) (c:cs) _ -> error "not a label"
gives me the error:
Occurs check: cannot construct the infinite type: t = A t When generalising the type(s) for `insert' Failed, modules loaded: none.
I can see why that would be, but what type should the final t be? Is there a way to get round it or is this type of thing restricted to the type-level only? Thanks, Jim
Manuel
Jim Burton:
Hi, I hope this is the right place to ask about working with type families...I want to make a library of Set operations that carries proofs at the type level, e.g. to make things like this possible,
insert :: Member e s' T => e -> Set s -> Set s' union :: Union s t u => Set s -> Set t -> Set u
The trouble is designing the Set datatype so it can be used in type constraints *and* in run-time functions....Something similar is of course possible with fun deps, and I knocked something up following the example of Conrad Parker's 'Instant Insanity' but, crucially, that code is 'trapped' in the type system with no populated types. I want term-level/run-time functions with enhanced constraints, such as in the example Manuel posted in haskell-cafe:
data Z data S a
data SNat n where Zero :: SNat Z Succ :: SNat n -> SNat (S n)
zero = Zero one = Succ zero
type family (:+:) n m :: * type instance Z :+: m = m type instance (S n) :+: m = S (n :+: m)
add :: SNat n -> SNat m -> SNat (n :+: m) add Zero m = m add (Succ n) m = Succ (add n m)
This seems like "the best of both worlds" -- maybe it could be a general strategy for making for making these enhanced constraints at the term-level? Make a (populated) GADT and parameterise it with a phantom type (perhaps amongst other things). Make a type operator that can be used to express the constraint on the phantom types carried around by the "regular" populated type. When the type operator appears in the codomain of the function it's a compile-time check on the implementation of that function and when in the domain it checks the user at run- time.
However, (SNat n) can be put very succinctly because it doesn't need to carry a value around other than the Peano number in the phantom type. What about Sets? In my case the values in the sets are just labels and could well be empty:
data A ; data B ; data C
And I also need to express the cons-ness -- I don't think that needs fancy constraints so it can be done with terms, e.g., an underlying sequence such as in the Collects example. Generally I need to work out what needs to be run-time and what compile-time but I think that would follow from getting the combinations of types and terms in the Set abstraction right...could someone give me a pointer with this?
Many thanks,
Jim
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
insert :: Char -> Set t Char -> Set t Char insert c (Set tinfo cs) = case c of 'A' -> Set (InsA tinfo) (c:cs) _ -> error "not a label"
gives me the error:
Occurs check: cannot construct the infinite type: t = A t When generalising the type(s) for `insert' Failed, modules loaded: none.
To do what you are trying to do, it seems that you would also need to be able to write a function whose return type depended on a simple parameter value: foo :: Char -> ??? Seems impossible. With GADTs, you can of course go the other way:
data A data B
data Chr a where AChr :: Chr A BChr :: Chr B
toChar :: Chr a -> Char toChar AChr = 'A' toChar BChr = 'B'
So perhaps insert should have a type something more like:
type family ChrSetIns a t :: *
insert :: Chr a -> ChrSet t -> ChrSet (ChrSetIns a t)
I'm not sure how to make the set type parametric in the element type, though.
On Sat, 2007-12-01 at 11:33 +1000, Matthew Brecknell wrote: [...]
Seems impossible. With GADTs, you can of course go the other way:
data A data B
data Chr a where AChr :: Chr A BChr :: Chr B
toChar :: Chr a -> Char toChar AChr = 'A' toChar BChr = 'B'
So perhaps insert should have a type something more like:
type family ChrSetIns a t :: *
insert :: Chr a -> ChrSet t -> ChrSet (ChrSetIns a t)
I'm not sure how to make the set type parametric in the element type, though.
Thanks -- I think I see your point but I'm not sure how to make use of it...(perhaps I'm trying to run before I can walk). The way I was picturing things, the A, B ... types would need to take a parameter so they can be collected/consed, so my next attempt tries to incorporate both ideas: data A data B data Nil data t ::: ts -- consing the phantom types data Chr a where AChr :: Chr A BChr :: Chr B toChar :: Chr a -> Char toChar AChr = 'A' toChar BChr = 'B' data TInfo t where Nil :: TInfo Nil InsA :: TInfo t -> TInfo (A ::: t) InsB :: TInfo t -> TInfo (B ::: t) data ChrSet t = ChrSet (TInfo t) [Char] type family ChrSetIns c s :: * type instance ChrSetIns (Chr a) (TInfo t) = TInfo (a ::: t) insert :: Chr a -> ChrSet t -> ChrSet (ChrSetIns a t) insert c (ChrSet tinfo cs) = case c of AChr -> ChrSet (InsA tinfo) ((toChar c):cs) _ -> error "not a label" `insert' is still the problem -- how to form the 1st param of ChrSet. (InsA tinfo) isn't an instance of ChrSetIns, but I don't see how to fix that...? The error: ------------------------------------------- Couldn't match expected type `ChrSetIns A t' against inferred type `A ::: t' Expected type: TInfo (ChrSetIns A t) Inferred type: TInfo (A ::: t) In the first argument of `ChrSet', namely `(InsA tinfo)' In the expression: ChrSet (InsA tinfo) ((toChar c) : cs) Failed, modules loaded: none. Thanks, Jim
Jim Burton said:
Thanks -- I think I see your point but I'm not sure how to make use of it...(perhaps I'm trying to run before I can walk). The way I was picturing things, the A, B ... types would need to take a parameter so they can be collected/consed, so my next attempt tries to incorporate both ideas:
[...]
I was imagining something more along the lines of this:
data A data B
data Chr a where AChr :: Chr A BChr :: Chr B
toChar :: Chr a -> Char toChar AChr = 'A' toChar BChr = 'B'
data Nil data t ::: ts
data ChrSet t where Nil :: ChrSet Nil Ins :: Chr a -> ChrSet t -> ChrSet (a ::: t)
insert :: Chr a -> ChrSet t -> ChrSet (a ::: t) insert = Ins
That, by itself, doesn't require type families. I imagine you'll need type families if you want to do things like implement a tree structure, perform membership tests, deletions, etc. Note that if you want to reason about the correctness of code in this way, your data structures need to carry proofs. For example, the ChrSet data type I've given above enforces the correspondence between the value-level representation and the type-level representation, so given any ChrSet, I know the type-level decomposition will reflect the value-level decomposition, regardless of where that ChrSet came from. On the other hand, the ChrSet you proposed in your previous post doesn't have this property: data ChrSet t = ChrSet (TInfo t) [Char] Given one of these, I can't be confident that the type reflects the value, without inspecting all of the code that might have contributed to its construction. And that defeats the purpose of your endeavours. So you should defer the call to toChar until the last possible moment, if you call it at all. Another thought occurred to me: you might want to construct a ChrSet from user input, which brings us back to the problem I described in my previous post. All is not lost, though. You'll just need to keep your Chr and ChrSet values inside existential boxes:
data ChrBox = forall a . ChrBox (Chr a)
fromChar :: Char -> ChrBox fromChar 'A' = ChrBox AChr fromChar 'B' = ChrBox BChr fromChar _ = error "fromChar: bad Char"
data ChrSetBox = forall t . ChrSetBox (ChrSet t)
insertChar :: Char -> ChrSetBox -> ChrSetBox insertChar c (ChrSetBox s) = case fromChar c of ChrBox c -> ChrSetBox (insert c s)
BTW, I think you might get more interesting responses to theses questions in haskell-cafe.
On Fri, 2007-11-30 at 13:37 +1100, Manuel M T Chakravarty wrote:
Whenever you want to maintain type-level assertions of properties of you functions, you need to decide *how much* of the value-level information do you need on the type level to express and check the properties that you are interested in.
Hope you don't mind me going back to this point Manuel; given that I want to maintain enough type-level information to provide correctness checks on the implementations of set operations and on their inputs, is this _impossible_ except at the extreme end of the spectrum? As you say below, I was hoping this would not be the case and that it would be possible to create something with those properties that could be used in an interactive setting. Your SNat example is a simpler case, but it pulls off that feat, which made me think it was a question of finding the right combination of types. Jim
My SNat example was at one extreme end of the spectrum: *complete* value-level information is reflected at the type level. In other case, it is only necessary to reflect partial information; eg, when reasoning about bounds-checks of bounded lists or arrays, only the length, but not the exact elements need to be reflected.
In other words, first you need to decide what properties you want to enforce and what information you need to decide those properties. Coming back to your set example, what properties do you want to enforce/check and what information do you need to do that? In the extreme case, you could reflect the entire contents of each set at the type-level using a singleton set type (and corresponding singleton types for the set elements). However, that also would mean that all your value-level set operations will already have to be completely executed by the type checker at compile time, which is probably not what you want.
Does this make sense?
Manuel
Jim Burton:
Hi, I hope this is the right place to ask about working with type families...I want to make a library of Set operations that carries proofs at the type level, e.g. to make things like this possible,
insert :: Member e s' T => e -> Set s -> Set s' union :: Union s t u => Set s -> Set t -> Set u
The trouble is designing the Set datatype so it can be used in type constraints *and* in run-time functions....Something similar is of course possible with fun deps, and I knocked something up following the example of Conrad Parker's 'Instant Insanity' but, crucially, that code is 'trapped' in the type system with no populated types. I want term-level/run-time functions with enhanced constraints, such as in the example Manuel posted in haskell-cafe:
data Z data S a
data SNat n where Zero :: SNat Z Succ :: SNat n -> SNat (S n)
zero = Zero one = Succ zero
type family (:+:) n m :: * type instance Z :+: m = m type instance (S n) :+: m = S (n :+: m)
add :: SNat n -> SNat m -> SNat (n :+: m) add Zero m = m add (Succ n) m = Succ (add n m)
This seems like "the best of both worlds" -- maybe it could be a general strategy for making for making these enhanced constraints at the term-level? Make a (populated) GADT and parameterise it with a phantom type (perhaps amongst other things). Make a type operator that can be used to express the constraint on the phantom types carried around by the "regular" populated type. When the type operator appears in the codomain of the function it's a compile-time check on the implementation of that function and when in the domain it checks the user at run- time.
However, (SNat n) can be put very succinctly because it doesn't need to carry a value around other than the Peano number in the phantom type. What about Sets? In my case the values in the sets are just labels and could well be empty:
data A ; data B ; data C
And I also need to express the cons-ness -- I don't think that needs fancy constraints so it can be done with terms, e.g., an underlying sequence such as in the Collects example. Generally I need to work out what needs to be run-time and what compile-time but I think that would follow from getting the combinations of types and terms in the Set abstraction right...could someone give me a pointer with this?
Many thanks,
Jim
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
participants (3)
-
Jim Burton -
Manuel M T Chakravarty -
Matthew Brecknell