model theory for type classes
On Thu, Aug 23, 2012 at 01:25:39PM +0100, Patrick Browne wrote:
If there is no model expansion could it be because of the constructor discipline, which only allows variables, and constructors in the LHS argument patterns.
Indeed, a variable name as a pattern on the LHS of a function definition has nothing to do with any names which might be in scope. It is simply a pattern which matches anything. I am not sure what (if anything) this says about model expansions.
constant::Int constant = (1::Int) fun1::Int -> Int fun1 (constant::Int) = 8
fun1 returns 8 for all inputs. The fact that fun1's definition uses the name 'constant' which happens to have the same name as something in scope is irrelevant. For example, this is precisely the same as the above: constant :: Int constant = 1 fun1 :: Int -> Int fun1 foo = 8 -Brent
On 8/23/12 1:02 PM, Patrick Browne wrote:
I am just not sure whether there is a model expansion from the super-class model to the subclass model.
If by "model expansion from..." you mean that there is a canonical/unique/special mapping from every superclass model to some subclass model, then the answer is no. Consider, for instance, applicative functors and monads. We have the (idealized) type classes: class Functor a where... class Functor a => Applicative a where... class Applicative a => Monad a where... However, there are strictly more Applicative instances than there are Monad instances. E.g., lists support an Applicative instance based on zip and an Applicative instance based on the cartesian product; however, only the latter of these can be extended to a Monad. Well, technically, that's only if we assume the appropriate laws are part of the theories defined by the type classes. Without this assumption every type class can be instantiated at every type (for every method f, define f = undefined). -- Live well, ~wren
participants (3)
-
Brent Yorgey -
Patrick Browne -
wren ng thornton