Re: Monads
Mark Carroll [EMAIL PROTECTED] wrote in article [EMAIL PROTECTED] in gmane.comp.lang.haskell.cafe: Omitting the typeclass bit, I'm trying to write something like (s1 - s2) - StateT s1 m () - StateT s2 m a - StateT s1 m a That is, it sequences two StateT computations, providing a way to translate from the first's state to the second to keep the chain going. Don't you need a (s2 - s1) function as well, to translate the final state back into StateT s1? -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig GW Bush: And when leaders make the wise and responsible choice, when they renounce terror and weapons of mass destruction, as Col. Ghadafi has now done, they serve the interest of their own people and they add to the security of all nations. http://www.tmealf.com/survey_form.htm ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Infinite types
On 2003-12-08T12:42:46-0800, Jeffrey A. Scofield wrote: b = () - (a, b) [...] I'm wondering how to tell, as a relative newcomer to Haskell, that they aren't allowed. I think the rule you're looking for is the following: Don't equate a type variable with something that contains that type variable. This is known as the occurs check. This rule prohibits equi-recursive types like b above, but not iso-recursive types like data List a = Nil | Cons a (List a) because the type List a is merely isomorphic to something containing List a, but not equal to it. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig International Human Rights Day * 2003-12-10 * http://www.un.org/rights/ What if All Chemists Went on Strike? (science fiction) http://www.iupac.org/publications/ci/2003/2506/iw3_letters.html signature.asc Description: Digital signature ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Hypothetical reasoning in type classes
On 2003-11-13T13:19:28-, Simon Peyton-Jones wrote: | From: [EMAIL PROTECTED] | | Has anyone thought about adding hereditary Harrop formulas, in other | words hypothetical reasoning and universal quantification, to the | instance contexts in the Hsakell type class system? Yes, absolutely. See http://research.microsoft.com/~simonpj/Papers/derive.htm Section 7, and Trifanov's paper at the Haskell Workshop 2003 Thanks for the pointers! I am now thinking about encoding SML-style module systems into Haskell using type classes with functional dependencies. For this purpose, I seem to need hereditary Harrop formulas in instance contexts. I wonder if such encodings have been proposed previously in the literature? The closest I was able to find is Kahl and Scheffczyk's paper at the 2001 Haskell Workshop. Thanks again, Ken -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Anytime I see something screech across a room and latch onto someones neck, and the guy screams and tries to get it off, I have to laugh, because what is that thing. [http://philip.greenspun.com/humor/deep-thoughts] signature.asc Description: Digital signature ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Hypothetical reasoning in type classes
Hello, Has anyone thought about adding hereditary Harrop formulas, in other words hypothetical reasoning and universal quantification, to the instance contexts in the Hsakell type class system? Just today (and not only today) I wanted to write instance definitions like instance (forall a. C a = D a) = E [a] where ... This is analogous to wanting to write a rank-2 dictionary constructor (forall a. C a - D a) - E [a] at the term level, but with type classes, this dictionary constructor should be applied automatically, in a type-directed fashion, at compile time. The theory behind such instance contexts doesn't seem so intractable; indeed it looks decidable to my cursory examination. The opreational intuition is that we would like the type checker to generate an eigenvariable a and perform hypothetical reasoning. I would also like to quantify universally over type classes; in other words, if ? is the kind of a type class constraint (aka a dictionary type; perhaps o would be a better choice of notation), then I would like to define not just types of kind *-*-? (aka type classes) or kind (*-*)-? (aka constructor classes), but also types of kind (*-?)-(*-?). But that's for another day... Ken -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Hi, my name is Kent, and I let people change my .sig on the internet. Hi, Ken! Put midgets back in midget porn! -- Not authorized by Ken Shan. Supported by the association of midget porn workers, Local 9823. signature.asc Description: Digital signature ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Type tree traversals [Re: Modeling multiple inheritance]
Brandon Michael Moore [EMAIL PROTECTED] wrote in article [EMAIL PROTECTED] in gmane.comp.lang.haskell.cafe: There are two extensions here: More overlapping: [...] Backtracking search: [...] Overloading resolution: [...] I'm sorry if I am getting ahead of Simon or behind of you, but have you looked at Simon L. Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: An exploration of the design space. In Proceedings of the Haskell workshop, ed. John Launchbury. http://research.microsoft.com/Users/simonpj/papers/type-class-design-space/ ? There is quite a bit of design discussion there, and I am not sure how much has been obsoleted by more recent advances. A primary consideration seems to be that the compiler should be guaranteed to terminate (so type checking must be decidable). -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig hqrtzdfg aooieoia pnkplptr ywwywyyw ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: can this be written more easily?
On 2003-02-21T13:37:26-0500, Mike T. Machenry wrote:
Eh, state is not possible. This is a recursive state space search. I need
to branch the state of the game and not allow branches to effect others.
I see-- so you don't care about performing array updates in place,
because you will be copying arrays from parent nodes in the state space
to child nodes anyway. Is that correct?
From what you originally wrote, it seems to me that you are forced
to write awkward code because very often you need to reach into a
data structure and perform some manipulation on a part of it without
affecting anything else. This seems like a common pattern that deserves
abstraction.
If you have a function from a to a, and you have an Array of a's, you
can apply that function to update a certain element of that Array:
atIndex :: (Ix i) = i - (a - a) - (Array i a - Array i a)
atIndex i f a = a // [(i, f (a!i))]
Similarly, whenever you have a tickets-to-tickets function (by the way, it
seems that you renamed tickets to dTickets or vice versa while composing
your message), you can turn it into a GameState transformer:
atTickets :: (Array Player (Array Ticket Int) -
Array Player (Array Ticket Int))
- (GameState - GameState)
atTickets f s = s { tickets = f (tickets s) }
Your removeTicket function can now be written
removeTicket s d t = (atTickets $ atIndex d $ atIndex t $ pred) s
This technique generalizes from arrays and records to other container
data structures like lists and finite maps.
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Is it because of problems at school that you say you hope the
eurythmics'' practice birth control?
pgp0.pgp
Description: PGP signature
Re: newbie questions
On 2003-01-08T09:19:10+0200, Max Ischenko wrote: - To be able to run it both in Hugs and by GHC I need an `import Data.Char(isSpace) for GHC`. Can this be conditionally included in a source for GHC only? You could use say the C preprocessor to do this, but a better way to solve your problem would be to say import Char (isSpace) This should work with Hugs, GHC, as well as other implementations of Haskell 98. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Studded tires buzzing Cycle to work all year, I See stupid people msg02426/pgp0.pgp Description: PGP signature
Re: Monad Maybe?
On 2002-09-21T12:56:13-0700, Russell O'Connor wrote: case (number g) of Just n - Just (show n) Nothing - case (fraction g) of Just n - Just (show n) Nothing - case (nimber g) of Just n - Just (*++(show n)) Nothing - Nothing How about something like: msum [ liftM show (number g) , liftM show (fraction g) , liftM ((*++).show) (nimber g) ] -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig So the choice which Lomborg presents us with, of whether to save a drowning Tuvaluan (climate change) or a dying Somalian (water and sanitation) is not a choice at all -- in fact we need to do both, and not least because one is unlikely to be successful without the other. http://www.anti-lomborg.com/ msg02004/pgp0.pgp Description: PGP signature
Re: Modification of State Transformer
On 2002-08-08T14:11:54-0500, Shawn P. Garbett wrote: newtype St a s = MkSt (s - (a, s)) instance Monad St where This line should say instance Monad (St a) where because it is (St a) that is a Monad, not St by itself. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig http://www.ethnologue.com/ msg01872/pgp0.pgp Description: PGP signature
Infix expressions
Hello, In Haskell, backquotes can be used to convert individual identifiers into infix operators, but not complex expressions. For example, [1,2,3] `zip` [4,5,6] is OK, but not [1,2,3] `zipWith (+)` [4,5,6] Is there any reason other than potential confusion when one of the two backquotes is accidentally omitted? In any case, perhaps some people on this mailing list would appreciate the following implementation of infix expressions that Dylan Thurston and I came up with -- as algebraic and perverse as we could manage: infixr 0 -:, :- data Infix f y = f :- y x -:f:- y = x `f` y main = print $ [1,2,3] -: zipWith (+) :- [4,5,6] -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig The trick is that there is no trick. msg01848/pgp0.pgp Description: PGP signature
Re: newtype/datatype (was efficiency)
A while ago, to help myself understand newtype, data, and strictness, I tried to write down how Haskell types correspond to lifted domains. Here is a cleaned-up version of my attempt. I am not sure that what follows is entirely correct -- please point out any errors. I would also appreciate comments or pointers to where this stuff is better described. In particular, I have not considered recursive types. Every type t in Haskell can be denotationally modeled by a complete partial order (CPO), which we will notate as [t]. In fact, every type in standard Haskell corresponds to a -pointed- CPO, meaning a CPO with a least element bottom. GHC, in addition, supports -unboxed- types, which correspond to CPOs in general. Given a CPO D, we can -lift- it to a pointed CPO lift D by adding a bottom. Given two (not necessarily pointed) CPOs D and E, we can take their -cartesian product- D x E, which is like the set-theoretic product. Given two pointed CPOs D and E, we can take their -smash product- D * E, which is like the set-theoretic/cartesian product, but which identifies all pairs of the form (x,bottom) or (bottom,y) into one single new bottom element. The identity of * is the two-element pointed CPO 1, which consists of a bottom and a top. Given two pointed CPOs D and E, we can take their -coalesced sum- D + E, which is like the set-theoretic sum, but which identifies the bottom from D and the bottom from E into one single new bottom element. The identity of + is the one-element pointed CPO 0, which consists only of a bottom. Given any two (not necessarily pointed) CPOs, we have the property lift D * lift E = lift (D x E). In Haskell, if you write newtype t' = T t-- , then [t'] is exactly isomorphic to [t]. Pattern matching on the T is a no-op (i.e., always succeeds). Now turn to a data declaration data t' = T1 ... | T2 ... | ... -- . Each branch in the declaration specifies a pointed CPO by naming zero or more data types, each of which can be strict or non-strict. We lift the non-strict ones, then take the smash product of everything. The result is the pointed CPO denoted by the branch. The pointed CPO [t'] denoted by the combined data type t' is the coalesced sum of the pointed CPOs denoted by all the branches. For example, if we write data t' = T1 !t11 !t12 | T2 t2 | T3 -- , then [t'] = [t11] * [t12] + lift [t2] + 1-- . Pattern-matching on any data-declared type such as t' above is always strict, in the sense that if the value being matched against is bottom, then the whole expression denotes bottom. For example, given how we defined t' above, the expression case x' of T1 _ _ - y T2 _ - y T3 - y is entirely equivalent to x' `seq` y -- . The only reason to have `seq` is because primitive types such as Int cannot be pattern-matched against. (Hence people call seq polymorphic case.) Unboxed types are non-pointed CPOs, so it doesn't make sense to say data t' = T !t if t is an unboxed type, but it does make sense to say data t' = T t because [t] can be lifted to a pointed CPO. You ought to be able to say newtype t' = T t to define a new unboxed type t' from an existing unboxed type t, but I faintly remember this being not implemented or allowed or something. Tuple types are special notation for what could be otherwise defined using data declarations as follows: data () = () data (,) t1 = (,) t1 data (,,) t1 t2= (,,) t1 t2 data (,,,) t1 t2 t3 = (,,,) t1 t2 t3 -- ... So we have [()] = 1 [(t1 )] = lift [t1] [(t1,t2 )] = lift [t1] * lift [t2] = lift ([t1] x [t2]) [(t1,t2,t3)] = lift [t1] * lift [t2] * lift [t3] = lift ([t1] x [t2] x [t3]) ... If [t1] has 3 elements including its bottom, and [t2] has 5 elements including its bottom, then [(t1,t2)] has 3 * 5 + 1 = 16 elements including its bottom. Given the definitions above, let us consider some corner and not so corner declarations: (When I write that foo denotes bar, I mean that foo denotes something isomorphic to bar.) data T1 -- denotes 0, the identity for + -- (but this is not standard Haskell) data T2 = T2-- denotes 1, the identity for * data T3 = T3 () -- denotes lift 1, because () denotes 1 data T4 = T4 !()-- denotes 1, because () denotes 1 newtype T5 = T5 () -- denotes 1, because () denotes 1 data T6 = T6 !T1 Int-- denotes 0 * lift [Int], which is just 0 Note that although both T4 and T5 denote 1, pattern-matching on them is different: case T4 undefined of T4 _ - y === undefined case T5 undefined of T5 _ - y === y Whew. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig and view Ken's picture at
Re: Funny type.
On 2001-05-27T22:46:37-0500, Jay Cox wrote: data S m a = Nil | Cons a (m (S m a)) instance (Show a, Show (m (S m a))) = Show (S m a) where show Nil = Nil show (Cons x y) = Cons ++ show x ++ ++ show y Here's how I've been handling such situations: data S m a = Nil | Cons a (m (S m a)) -- ShowF f means that the functor f preserves Show class ShowF f where showsPrecF :: (Int - a - ShowS) - (Int - f a - ShowS) -- instance ShowF [] is based on showList instance ShowF [] where showsPrecF sh p [] = showString [] showsPrecF sh p (x:xs) = showChar '[' . sh 0 x . showl xs where showl [] = showChar ']' showl (x:xs) = showChar ',' . sh 0 x . showl xs -- S preserves ShowF instance (ShowF m) = ShowF (S m) where showsPrecF sh p Nil = showString Nil showsPrecF sh p (Cons x y) = showString Cons . sh 0 x . showChar ' ' . showsPrecF (showsPrecF sh) 0 y -- Now we can define instance Show (S m a) as desired instance (Show a, ShowF m) = Show (S m a) where showsPrec = showsPrecF showsPrec You could call it the poor man's generic programming... -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig My SUV is bigger than your bike. Stay out of the damn road! Kiss my reflector, SUV-boy I'm too busy sucking on my tailpipe, bike dude. PGP signature
