Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: How to avoid repeating a type restriction from a data
constructor (gs)
2. Re: How to avoid repeating a type restriction from a data
constructor (Daniel Fischer)
3. Re: How to avoid repeating a type restriction from a data
constructor (gs)
4. Re: How to avoid repeating a type restriction from a data
constructor (gs)
5. Re: How to avoid repeating a type restriction from a data
constructor (Daniel Fischer)
6. Re: How to avoid repeating a type restriction from a data
constructor (Daniel Fischer)
7. Re: How to avoid repeating a type restriction from a data
constructor (gs)
8. Re: How to avoid repeating a type restriction from a data
constructor (gs)
----------------------------------------------------------------------
Message: 1
Date: Wed, 24 Apr 2013 16:45:35 +0000 (UTC)
From: gs <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> Well, the context is not redundant, that's the crux.
>
> You can specify the type `Source v a` even when there is no `Variable v`
> instance [whether you use DatatypeContexts - which, again, are pretty useless
> because they don't do what one would expect - or GADTs]. And such a type is
> inhabited by bottom, you just can't create non-bottom values of such a type.
>
> Hence the `Variable v` context gives additional information that is needed
for
> the instance.
I'm not following - perhaps you could give a practical example? I'm trying
to understand the flaw in this:
1) The compiler sees that a Source v a can only be created when v is a variable.
2) Whenever Source v a is used, the compiler should understand that v is a
variable without me having to remind it.
------------------------------
Message: 2
Date: Wed, 24 Apr 2013 19:34:38 +0200
From: Daniel Fischer <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: [email protected]
Cc: gs <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="us-ascii"
On Wednesday 24 April 2013, 16:45:35, gs wrote:
> Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> > Well, the context is not redundant, that's the crux.
> >
> > You can specify the type `Source v a` even when there is no `Variable v`
> > instance [whether you use DatatypeContexts - which, again, are pretty
> > useless because they don't do what one would expect - or GADTs]. And such
> > a type is inhabited by bottom, you just can't create non-bottom values of
> > such a type.
> >
> > Hence the `Variable v` context gives additional information that is needed
>
> for
>
> > the instance.
>
> I'm not following - perhaps you could give a practical example? I'm trying
> to understand the flaw in this:
>
> 1) The compiler sees that a Source v a can only be created when v is a
> variable.
No, that is the catch:
undefined :: Source NotAnInstanceOfVariable Int
is possible.
> 2) Whenever Source v a is used, the compiler should understand
> that v is a variable without me having to remind it.
But when you use the value constructor,
foo (Source list var) = ...
you know that the `v` parameter of the type must have a Variable instance.
When you use a GADT, the compiler knows that too and can use that fact, when
you use DatatypeContexts, the compiler can't use that knowledge (even though
it has the knowledge).
The point is that the type class dictionary is required to use the class
methods, and with a GADT, the dictionary is bundled with the constructor, so
pattern-matching makes the dictionary available.
Not so with DatatypeContexts, hence the dictionary must be explicitly passed
with the context on the function.
Did I already mention that DatatypeContexts are fairly useless and have
therefore been removed from the language?
------------------------------
Message: 3
Date: Wed, 24 Apr 2013 18:34:07 +0000 (UTC)
From: gs <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> No, that is the catch:
>
> undefined :: Source NotAnInstanceOfVariable Int
>
> is possible.
OK, I've got that. Now let's say that
data Source v a = Variable v => Source {bindings :: v [Binding a], var :: v a}
or
data Variable v => Source v a = Source {bindings :: v [Binding a], var :: v a}
instance Variable (Source v) where
newVar a = do bindings <- newVar []
v <- newVar a
return $ Source bindings v
was allowed - then newVar (undefined :: Source NotAnInstanceOfVariable Int)
would then attempt newVar (?? :: NotAnInstanceOfVariable), which doesn't
type check, because newVar only works on Variables.
Is this correct? If that's the only problem, it doesn't seem like much of a
loss, as even with the type context, undefined :: Source
SomeInstanceOfVariable Int isn't going to be of much use either.
------------------------------
Message: 4
Date: Wed, 24 Apr 2013 18:39:15 +0000 (UTC)
From: gs <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> The point is that the type class dictionary is required to use the class
> methods, and with a GADT, the dictionary is bundled with the constructor, so
> pattern-matching makes the dictionary available.
>
> Not so with DatatypeContexts, hence the dictionary must be explicitly passed
> with the context on the function.
So is this more of an implementation issue? No "real" ill-typed programs
will get through the type checker if the compiler could remember the type
dictionary without pattern-matching or explicit context?
------------------------------
Message: 5
Date: Wed, 24 Apr 2013 22:12:12 +0200
From: Daniel Fischer <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="us-ascii"
On Wednesday 24 April 2013, 18:34:07, gs wrote:
> Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> > No, that is the catch:
> >
> > undefined :: Source NotAnInstanceOfVariable Int
> >
> > is possible.
>
> OK, I've got that. Now let's say that
>
> data Source v a = Variable v => Source {bindings :: v [Binding a], var :: v
> a} or
> data Variable v => Source v a = Source {bindings :: v [Binding a], var :: v
> a}
>
> instance Variable (Source v) where
> newVar a = do bindings <- newVar []
> v <- newVar a
> return $ Source bindings v
>
> was allowed - then newVar (undefined :: Source NotAnInstanceOfVariable Int)
> would then attempt newVar (?? :: NotAnInstanceOfVariable), which doesn't
> type check, because newVar only works on Variables.
The type annotations here are wrong, since
newVar :: a -> IO (v a)
But yes, the problem is that the `newVar` implementation for `Source` uses the
`newVar` implementation for `v`, hence
newVar :: a -> IO (Source NotAnInstance Int)
would be a type error.
If the type was changed to
newVar :: v a -> a -> IO (v a)
newVar dummy value = old_implementation_ignoring_dummy
you could write an
instance Variable (Source v) where
newVar (Source _ _) value = do
binds <- newVar []
v <- newVar value
return (Source binds v)
with the GADT, since you get the Variable instance of the `v` parameter by
pattern-matching on the dummy argument. For some
Source NotAnInstance whatever
type (such a type has no non-bottom values), `newVar` would be undefined.
>
> Is this correct? If that's the only problem, it doesn't seem like much of a
> loss, as even with the type context, undefined :: Source
> SomeInstanceOfVariable Int isn't going to be of much use either.
The problem is that you can only write a useful instance if you can somehow
access a useful Variable instance for the `v` parameter.
Without an instance context or pattern-matching, the only possible
implementations are variants of undefined.
------------------------------
Message: 6
Date: Wed, 24 Apr 2013 22:18:51 +0200
From: Daniel Fischer <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="us-ascii"
On Wednesday 24 April 2013, 18:39:15, gs wrote:
> Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> > The point is that the type class dictionary is required to use the class
> > methods, and with a GADT, the dictionary is bundled with the constructor,
> > so pattern-matching makes the dictionary available.
> >
> > Not so with DatatypeContexts, hence the dictionary must be explicitly
> > passed with the context on the function.
>
> So is this more of an implementation issue? No "real" ill-typed programs
> will get through the type checker if the compiler could remember the type
> dictionary without pattern-matching or explicit context?
It's an implementation issue, yes. But DatatypeContexts were specified so that
an implementation wasn't allowed to make the dictionary available without
context.
I don't remember the details, but there are good reasons why GADTs make the
dictionaries only available on pattern-matching, part of it is that with
GADTs, you get type refinement, the constructor matched against is used to
further refine and restrict or instantiate type variables in the function
signature. It could work without pattern-matching for single-constructor
GADTs, I think, but that would require a special case for dubious benefit.
------------------------------
Message: 7
Date: Thu, 25 Apr 2013 07:39:10 +0000 (UTC)
From: gs <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> It's an implementation issue, yes. But DatatypeContexts were specified so
that
> an implementation wasn't allowed to make the dictionary available without
> context.
Thank you for your patience in explaining everything. It's a pity that
DatatypeContexts don't do this - it would make my code much cleaner.
------------------------------
Message: 8
Date: Thu, 25 Apr 2013 08:03:25 +0000 (UTC)
From: gs <[email protected]>
Subject: Re: [Haskell-beginners] How to avoid repeating a type
restriction from a data constructor
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
Daniel Fischer <daniel.is.fischer <at> googlemail.com> writes:
> ...
You've mentioned GADT a few times, but I can't find a case where it's
different to regular datatypes.
data Foo a = Eq a => Foo a
seems to have the same effect as
data Foo a where
Foo a :: Eq a => a -> Foo a
Both remember the Eq constraint if I pattern match on the constructor, and
both ignore it otherwise.
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 58, Issue 38
*****************************************
