Re: termination for FDs and ATs
Thanks for clarifying this. On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote: So, we get the following type for f f :: (Mul a b, [Result a b] = b) = Bool - a - b - [Result a b] Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f. That would be the case if the definition were f b x y = if b then x .*. [y] else y You'd assign f a type with unsatisfiable constraints, obtaining termination by deferring the check. But the definition f = \ b x y - if b then x .*. [y] else y will presumably be rejected, because you won't infer the empty context that the monomorphism restriction demands. So the MR raises the reverse question: can you be sure that every tautologous constraint is reducible? So, clearly termination for ATs and FDs is *not* the same. It's quite interesting to have a close look at where the difference comes from. The FD context corresponding to (*) above is Mul a [b] b Improvement gives us Mul a [[c]] [c] with b = [c] which simplifies to Mul a [c] c which is where we loop. The culprit is really the new type variable c, which we introduce to represent the result of the type function encoded by the type relation Mul. So, this type variable is an artifact of the relational encoding of what really is a function, It's an artifact of the instance improvement rule, but one could define a variant of FDs without that rule. Similarly one could have a variant of ATs that would attempt to solve the equation [Result a b] = b by setting b = [c] for a fresh variable c. In both cases there is the same choice: defer reduction or try for more precise types at the risk of non-termination for instances like these. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: raw data access
On Tue, May 02, 2006 at 12:57:17AM +0200, Johan Henriksson wrote: toBinary :: a - [Int] -- pack data as a string of bytes fromBinary :: [Int] - a -- unpack binarySize :: a - Maybe Int -- number of bytes for this type or Nothing if not fixed the packing would be compiler dependent since it is not of interest to read the content, just to get an easy way of marshalling arbitrary types. Depending on what you mean, we might already have this, or it might be impossible in general :) if you just want to create a reference to an arbitrary haskell type that you can pass to foreign code, and then recover the original haskell value from, then the Foreign.StablePtr does just this. it lets you cast haskell values to plain pointers and back again. if you want to store the structure in memory, then the Storable class provides this. I have thought it would be useful to allow deriving(Storable) with the obvious meaning and adding a 'StorableRef' that can create a reference to an arbitray storable object. I believe bulat is working on unboxed arrays that can work like this. of course, the limitation is that your data types need to be in class Storable. since you don't seem to care about compiler independence and if you are willing to give up architecture independence, you can probably use storable to serialize structures to disk, but do so at your own risk. pretty much any solution will require a typeclass to guide and restrict it, otherwise how would the compiler handle function types? it can't serialize the body of functions in general, or handle cyclic structures or pointers from the serialized version to live haskell structures and how they interect with the GC? You also might want to look at the various Binary libraries out there. perhaps one fits your needs. John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: termination for FDs and ATs
On Sat, Apr 29, 2006 at 07:13:28PM -0400, Manuel M T Chakravarty wrote: 1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) However they are under consideration for Haskell', so it would be worth knowing whether they would create future problems for ATs. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: WordPtr,IntPtr,IntMax,WordMax
On 2006-04-29, Manuel M T Chakravarty [EMAIL PROTECTED] wrote: Am Donnerstag, den 06.04.2006, 16:37 -0700 schrieb John Meacham: On Thu, Apr 06, 2006 at 04:28:01PM -0700, John Meacham wrote: I was curious if ghc could support the following basic types, they will likely just be aliases of existing types. WordPtr uintptr_t WordMax uintmax_t IntPtr intptr_t IntMax intmax_t all these C types are defined by ISO C so should be available, otherwise, they are easy enough to generate in ghcs autoconf script. jhc provides these under these names in Data.Word and Data.Int. they would be useful for writing jhc/ghc portable low level code, and writing 32/64 bit safe code. oh, I forgot the all important conversion routines, ptrToWordPtr :: Ptr a - WordPtr wordPtrToPtr :: WordPtr - Ptr a ptrToIntPtr :: Ptr a - IntPtr intPtrToPtr :: IntPtr - Ptr a jhc makes these available in Jhc.Addr, but if ghc decides to provide them in a common spot (Foreign.Ptr maybe?) then I will have jhc follow suit. I'd also propose these be added to the FFI standard. I collect additions to the FFI on the Haskell' wiki: http://hackage.haskell.org/trac/haskell-prime/wiki/ForeignFunctionInterface I added a note about these types. Any other ISO C types that we should include? complex foo. -- Aaron Denney -- ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: termination for FDs and ATs
Ross Paterson writes: Thanks for clarifying this. On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote: So, we get the following type for f f :: (Mul a b, [Result a b] = b) = Bool - a - b - [Result a b] Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f. That would be the case if the definition were f b x y = if b then x .*. [y] else y You'd assign f a type with unsatisfiable constraints, obtaining termination by deferring the check. But the definition f = \ b x y - if b then x .*. [y] else y will presumably be rejected, because you won't infer the empty context that the monomorphism restriction demands. So the MR raises the reverse question: can you be sure that every tautologous constraint is reducible? So, clearly termination for ATs and FDs is *not* the same. It's quite interesting to have a close look at where the difference comes from. The FD context corresponding to (*) above is Mul a [b] b Improvement gives us Mul a [[c]] [c] with b = [c] which simplifies to Mul a [c] c which is where we loop. The culprit is really the new type variable c, which we introduce to represent the result of the type function encoded by the type relation Mul. So, this type variable is an artifact of the relational encoding of what really is a function, It's an artifact of the instance improvement rule, but one could define a variant of FDs without that rule. Similarly one could have a variant of ATs that would attempt to solve the equation [Result a b] = b by setting b = [c] for a fresh variable c. In both cases there is the same choice: defer reduction or try for more precise types at the risk of non-termination for instances like these. I agree. At one stage, GHC (forgot which version) behaved similarly compared to Manuel's AT inference strategy. Manuel may have solved the termination problem (by stopping after n number of steps). Though, we still don't know yet whether the constraints are consistent. One of the reasons why FD *and* AT inference is tricky is because inference may be non-terminating although - type functions/FD improvements are terminating - type classes are terminating We'll need a more clever analysis (than a simple occurs check) to reject 'dangerous' programs. Martin ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: termination for FDs and ATs
Manuel M T Chakravarty writes: Martin Sulzmann: A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs. Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html The message that you are citing here has two problems: 1. You are using non-standard instances with contexts containing non-variable predicates. (I am not disputing the potential merit of these, but we don't know whether they apply to Haskell' at this point.) 2. You seem to use the super class implication the wrong way around (ie, as if it were an instance implication). See Rule (cls) of Fig 3 of the Associated Type Synonyms paper. I'm not arguing that the conditions in the published AT papers result in programs for which inference is non-terminating. We're discussing here a possible AT extension for which inference is clearly non-terminating (unless we cut off type inference after n number of steps). Without these extensions you can't adequately encode the MonadReader class with ATs. This plus the points that I mentioned in my previous two posts in this thread leave me highly unconvinced of your claims comparing AT and FD termination. As argued earlier by others, we can apply the same 'tricks' to make FD inference terminating (but then we still don't know whether the constraint store is consistent!). To obtain termination of type class inference, we'll need to be *very* careful that there's no 'devious' interaction between instances and type functions/improvement. It would be great if you could come up with an improved analysis which rejects potentially non-terminating AT programs. Though, note that I should immediately be able to transfer your results to the FD setting based on the following observation: I can turn any AT proof into a FD proof by (roughly) - replace the AT equation F a=b with the FD constraint F a b - instead of firing type functions, we fire type improvement and instances - instead of applying transitivity, we apply the FD rule F a b, F a c == b=c Similarly, we can turn any FD proof into a AT proof. Martin ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
