RE: [Haskell-cafe] checking types with type families

2010-07-07 Thread Simon Peyton-Jones
Martin Sulzmann, Jeremy Waznyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.html, Peter J. Stuckeyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_J=.html: A Framework for Extended Algebraic Data Types. FLOPS

Re: [Haskell-cafe] checking types with type families

2010-07-07 Thread C. McCann
On Sat, Jul 3, 2010 at 4:28 PM, Dan Doel dan.d...@gmail.com wrote: It's potentially not just a violation of intent, but of soundness. The following code doesn't actually work, but one could imagine it working:  class C a b | a - b  instance C () a  -- Theoretically works because C a b, C a

Re: [Haskell-cafe] checking types with type families

2010-07-03 Thread Kevin Quick
On Wed, 23 Jun 2010 00:14:03 -0700, Simon Peyton-Jones simo...@microsoft.com wrote: I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). Simon, I have run into

Re: [Haskell-cafe] checking types with type families

2010-07-03 Thread David Menendez
On Sat, Jul 3, 2010 at 3:32 AM, Kevin Quick qu...@sparq.org wrote: On Wed, 23 Jun 2010 00:14:03 -0700, Simon Peyton-Jones simo...@microsoft.com wrote: I'm interested in situations where you think fundeps work and type families don't.  Reason: no one knows how to make fundeps work cleanly with

Re: [Haskell-cafe] checking types with type families

2010-07-03 Thread Dan Doel
On Saturday 03 July 2010 2:11:37 pm David Menendez wrote: {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances #-} class C a b c | a - b, a - c where op :: a - b - c instance C Bool a a where op _ =

Re: [Haskell-cafe] checking types with type families

2010-07-03 Thread Kevin Quick
On Sat, 03 Jul 2010 12:48:56 -0700, Dan Doel dan.d...@gmail.com wrote: Then the instance declares infinitely many instances C Bool a a. This is a violation of the fundep. Based on your error message, it looks like it ends up treating the instance as the first concrete 'a' it comes across, but

Re: [Haskell-cafe] checking types with type families

2010-07-03 Thread Dan Doel
On Saturday 03 July 2010 4:01:12 pm Kevin Quick wrote: As a side note, although I agree it abuses the fundeps intent, it was handy for the specific purpose I was implementing to have a no-op/passthrough instance of op. In general I like the typedef approach better, but it looks like I must

Re: [Haskell-cafe] checking types with type families

2010-07-03 Thread Kevin Quick
On Sat, 03 Jul 2010 13:28:44 -0700, Dan Doel dan.d...@gmail.com wrote: As a side note, although I agree it abuses the fundeps intent, it was handy for the specific purpose I was implementing to have a no-op/passthrough instance of op. In general I like the typedef approach better, but it

RE: [Haskell-cafe] checking types with type families

2010-07-01 Thread Simon Peyton-Jones
| Here's a concrete case I recently ran into: | | type family SomeOtherTypeFamily a | class SomeClass a where type SomeType a | instance a ~ SomeOtherTypeFamily b = SomeClass a where |type SomeType a = (b,Int) |-- (error) Not in scope: type variable `b' | | The same thing

RE: [Haskell-cafe] checking types with type families

2010-07-01 Thread Simon Peyton-Jones
Claus | I'm interested in situations where you think fundeps work | and type families don't. Reason: no one knows how to make | fundeps work cleanly with local type constraints (such as GADTs). | | If you think you have such as case, do send me a test case. | | Do you have a wiki

RE: [Haskell-cafe] checking types with type families

2010-07-01 Thread Simon Peyton-Jones
| Well, from looking at the documentation, it looks like I could maybe | use a type family if I could write: | | class (DerivedOf a ~ derived) = Typecheck a derived where | ... That's the right idiom yes. But see my message of a few minutes ago... It's neater still to remove the

Re: [Haskell-cafe] checking types with type families

2010-07-01 Thread Martin Sulzmann
On Thu, Jul 1, 2010 at 7:54 PM, Simon Peyton-Jones simo...@microsoft.comwrote: | Also, what is the difference between fundeps and type families | wrt local type constraints? I had always assumed them to be | equivalent, if fully implemented. Similar to logic vs functional | programming,

RE: [Haskell-cafe] checking types with type families

2010-07-01 Thread Eduard Sergeev
Simon Peyton-Jones wrote: I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. As an example, is

Re: [Haskell-cafe] checking types with type families

2010-06-23 Thread Evan Laforge
I think your problem here is that there's no mention of `a' on the left-hand size of from_val's type signature; you either need to use MPTC+fundep to associate what result is compared to a, or else use a phantom type parameter of Val to make it data Val result a = ... and then from_val :: Val

RE: [Haskell-cafe] checking types with type families

2010-06-23 Thread Simon Peyton-Jones
| I think your problem here is that there's no mention of `a' on the | left-hand size of from_val's type signature; you either need to use | MPTC+fundep to associate what result is compared to a, or else use a | phantom type parameter of Val to make it data Val result a = ... and | then

Re: [Haskell-cafe] checking types with type families

2010-06-23 Thread Evan Laforge
I'm interested in situations where you think fundeps work and type families don't.  Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. Well, from looking at the documentation, it

Re: [Haskell-cafe] checking types with type families

2010-06-23 Thread Claus Reinke
I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs). If you think you have such as case, do send me a test case. Do you have a wiki page somewhere collecting

Re: [Haskell-cafe] checking types with type families

2010-06-22 Thread Ivan Miljenovic
On 23 June 2010 13:46, Evan Laforge qdun...@gmail.com wrote: I have a parameterized data type: data Val result = VNum Double | VThunk (SomeMonad result) type Environ result = Map Symbol (Val result) I have a class to make it easier to typecheck Vals: class Typecheck a where   from_val ::

Re: [Haskell-cafe] checking types with type families

2010-06-22 Thread Daniel Fischer
On Wednesday 23 June 2010 05:46:46, Evan Laforge wrote: I have a parameterized data type: data Val result = VNum Double | VThunk (SomeMonad result) type Environ result = Map Symbol (Val result) I have a class to make it easier to typecheck Vals: class Typecheck a where from_val :: Val