Re: termination for FDs and ATs
On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote: > Yes, FDs and ATs have the exact same problems when it comes to termination. > The difference is that ATs impose a dynamic check (the occurs check) > when performing type inference (fyi, such a dynamic check is sketched > in a TR version of the FD-CHR paper). Isn't an occurs check unsafe when the term contains functions (type synonyms)? You might reject something that would have been accepted if the function had been reduced and discarded the problematic subterm. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: termination for FDs and ATs
Ross Paterson writes: > On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote: > > Yes, FDs and ATs have the exact same problems when it comes to termination. > > The difference is that ATs impose a dynamic check (the occurs check) > > when performing type inference (fyi, such a dynamic check is sketched > > in a TR version of the FD-CHR paper). > > Isn't an occurs check unsafe when the term contains functions (type > synonyms)? You might reject something that would have been accepted > if the function had been reduced and discarded the problematic subterm. > Correct. Any dynamic check is necessarily incomplete. Martin ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Class ATs Question
You can do two-way fundeps. Can these be done with associated types? For instance: class HasSign u s | u -> s, s -> u where unsignedToSigned :: u -> s signedToUnsigned :: s -> u instance HasSign Word8 Int8 where ... It might not be a great loss if not. -- Ashley Yakeley, Seattle WA WWEWDD? http://www.cs.utexas.edu/users/EWD/ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
