Re: Type Families and enhanced constraints (at run-time)
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. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type Families and enhanced constraints (at run-time)
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. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Cost of Overloading vs. HOFs
Stefan O'Rear: Data.Sequence doesn't use overloading Data.Sequence uses overloading for subtree size annotations. The structural recursion seems to make it quite awkward to express size annotations without overloading. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT + Newtype deriving = Erroneous errors
Stefan O'Rear: They are the same type, and I have Curry-Howard proof of this fact. If that's the case, then it begs the question why you'd bother defining Foo in the first place. How would this solve EnumMap performance concerns? I am under the impression that newtypes are *defined* to be distinct types which don't unify. You haven't shown us your proof, but if it contradicts the definition, then it probably says more about the definition (or some other construct you've used) than any implementation derived from it. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Duplicate instance declarations of a methodless class
Alfonso Acosta: Did you try to compile with -fallow-overlapping-instances mm [EMAIL PROTECTED]: Same effect: ghc -fallow-overlapping-instances --make test5.lhs [1 of 1] Compiling Main ( test5.lhs, test5.o ) test5.lhs:22:1: Duplicate instance declarations: instance [overlap ok] (Succ a b) = GT a b -- Defined at test5.lhs:22:1 instance [overlap ok] (Succ a b, GT b c) = GT a c -- Defined at test5.lhs:23:1 Also see Oleg's post in this thread: http://www.haskell.org/pipermail/haskell-cafe/2007-February/022926.html ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
