headers
Brigitte Pientka | 3 Oct 2009 03:46
Picon
Favicon

Release of Beluga prototype

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear all,

 we'd like to announce the first release of Beluga.

The Beluga implementation provides an implementation of the logical
framework LF, and in addition a functional programming environment
which supports dependent types and analyzing LF data via pattern
matching. It is a completely new implementation effort. Its
implementation of the logical framework LF in OCaml shares, adapts and
extends some fundamental ideas from the Twelf system. The functional
programming environment which is built on top of the logical framework
LF is a completely new implementation based on previous theoretical
ideas presented in [Pientka:POPL08] and [PientkaDunfield:PPDP08].

At this point our prototype supports type reconstruction for LF
signatures as well as type reconstruction for dependently typed
functional programs over LF data.

To get a feel for Beluga, you can download our prototype together with
examples and the papers describing the foundation from

 http://complogic.cs.mcgill.ca/beluga/

Comments, questions, and bugs should be sent to
beluga-dev@...

Best,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Brian Hulley | 6 Oct 2009 01:15

A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi everyone,
with regards to the integration of Haskell-style typeclasses into an SML-style module system I've come
across a really difficult problem caused by the interaction of GADTs and scoped type-class instances,
and am wondering if anyone has any ideas on how it might be solved.

Consider the following Haskell module that compiles under ghc 6.8.2 with -fglasgow-exts enabled:

  module Test where
     data G a where
        Ok      :: forall a. Num a => a -> G ()
        Problem :: forall a. Num a => a -> G a

     analyse :: forall a. (G a, G a) -> a
     analyse (Ok x, Ok y)           = ()
     analyse (Ok x, Problem y)      = ()
     analyse (Problem x, Ok y)      = ()
     analyse (Problem x, Problem y) = x + y

  $ ghci -fglasgow-exts test.hs
  GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
  Loading package base ... linking ... done.
  [1 of 1] Compiling Test             ( test.hs, interpreted )
  Ok, modules loaded: Test.
  *Test> analyse (Problem (1 :: Int), Problem (2 :: Int))
  3
  *Test> Leaving GHCi.

Conceptually, the Problem constructor stores a Num dictionary for the type of its value argument, so in the
(Continue reading)

Permalink | Reply | 11 comments |
headers
Karl Crary | 6 Oct 2009 17:21
Picon
Favicon

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Brian,

Basically you're observing that a qualified GADT package includes an 
instance declaration, so unpacking it amounts to a using declaration.  
Accordingly, the "Problem" clause of your code would need to be treated 
as a using declaration, and it would be rejected for introducing 
overlapping instances.

It strikes me that in GHC you might well have the same problem with the 
"Ok" constructor.  A qualified existential package also includes an 
instance declaration, and unpacking it too amounts to a using 
declaration.  That ought not be a problem because it's an instance for 
an abstract type, so it cannot overlap any existing instances.  But, my 
understanding is that internally GHC does not really support abstract 
types, so that might not help.

By the way, I think that this issue exposes a design flaw in GADTs.  
GADTs provide a convenient way to do dynamic type analysis by 
integrating type representations into the datatype mechanism.  But, I 
think it's a mistake for GADTs to use actual types for those type 
representations.  Conceptually, the indices for a GADT are data, not 
sets of terms.  A better way to do GADTs would be to introduce a 
"datakind" mechanism, and use algebraic data kinds as the indices for a 
GADT.  You can get a picture of what this would look like from my 1999 
paper "Flexible Type Analysis" with Stephanie Weirich.  (That paper 
didn't have the tie-in with datatypes, which was invented later.)

The relevance to modular type classes is this:  If the index for a GADT
(Continue reading)

Permalink | Reply | 10 comments |
headers
Stefan Monnier | 6 Oct 2009 19:27
Picon

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> It strikes me that in GHC you might well have the same problem with the 
> "Ok" constructor.  A qualified existential package also includes an 
> instance declaration, and unpacking it too amounts to a using 
> declaration.  That ought not be a problem because it's an instance for 
> an abstract type, so it cannot overlap any existing instances.  But, my 
> understanding is that internally GHC does not really support abstract 
> types, so that might not help.

Actually, since GHC uses a variant of System F internally, it should
have no trouble supporting real abstract types.

> By the way, I think that this issue exposes a design flaw in GADTs.
> GADTs provide a convenient way to do dynamic type analysis by
> integrating type representations into the datatype mechanism.  But, I
> think it's a mistake for GADTs to use actual types for those type
> representations.  Conceptually, the indices for a GADT are data, not
> sets of terms.

I presume you're talking about GHC's GADTs.  As it turns out, they
are not specifically indexed by types of kind * (aka Ω), instead they
can be indexed by type expressions of pretty much any kind.

> A better way to do GADTs would be to introduce a "datakind" mechanism,
> and use algebraic data kinds as the indices for a GADT.

If GHC had datakinds, then its GADTs would support them as well.
I.e. you're talking about a design flaw of GHC/Haskell rather than its
GADTs which just happen to inherit it.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Brian Hulley | 7 Oct 2009 02:52

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Karl Crary wrote:
> Hi Brian,
> 
> Basically you're observing that a qualified GADT package includes an 
> instance declaration, so unpacking it amounts to a using declaration.  
> Accordingly, the "Problem" clause of your code would need to be treated 
> as a using declaration, and it would be rejected for introducing 
> overlapping instances.

Hi Karl,

Thanks for pointing out that the compiler could just reject this clause: perhaps this would be an
acceptable penalty to pay for the advantages of having scoped instances. However there are situations
where it would not be so clear what the compiler should do eg:

    bar :: forall a. G a -> (a, Int)
    bar (Problem x) = (x + x, 1 + 2)
    bar (Ok _)      = ((), 0)

In the expression (x + x, 1 + 2), what instance should the compiler use for (1 + 2)? Since (bar) is polymorphic,
the compiler, when compiling (bar), has no way of knowing whether or not the match against (Problem x) is
going to introduce a Num Int dictionary.

Of course this could be rejected on the grounds that the match *may* introduce an overlapping instance, or
we could restrict (a) so that it may not be instantiated to Int eg:

    bar :: forall a. (NotEqual Int a) => G a -> (a, Int)
(Continue reading)

Permalink | Reply | 5 comments |
headers
Brian Hulley | 7 Oct 2009 05:28

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Sameer Sundresh wrote:
> Brian Hulley wrote:
>> However in a modular setting, there is no such guarantee, so when
>> compiling (x + y) there would be an ambiguity about which Num Int
>> dictionary to use e.g.:
>>
>>
>>    structure P1 = struct
>>       instance Num Int where ...
>>
>>       val p1 : G Int = Problem 1
>>
>>    structure P2 = struct
>>       instance Num Int where ...
>>
>>       val p2 : G Int = Problem 2 (* different dictionary from p1 *)
>>
>>    structure Client = struct
>>
>>       val x = analyse (p1, p2)   (* 2 different dicts for Num Int *)
> 
> 
> When we're type checking the Client module, how do we know that Int has 
> been declared as an instance of Num?  Are you assuming there is also a 
> global instance Num Int, and P1 and P2 are locally overriding it?
> 
> - If yes, would it be acceptable to use the global instance declaration 
> for Num Int within module Client?
(Continue reading)

Permalink | Reply | 0 comments |
headers
Simon Peyton-Jones | 7 Oct 2009 10:15
Picon
Favicon
Gravatar

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I agree with Brian's analysis: the 'Problem' constructor is only ok because any way of satisfying a Num
constraint is as good as any other.   

The ability to have a data constructor capture a constraint of a *non-existential* type variable is newish
in GHC.  I added it for several reasons.  Firstly, it is more uniform.  It's great to be able to say "You can give
a constructor any old type, with arbitrary constraints".  Secondly, it's useful,  You can have, the
constructor for (Set a) capturing the (Ord a) constraint, eg
   data Set a where
      S :: forall a. Ord a => [a]
so that union can have type union :: Set a -> Set a -> Set a.  (Empty set is another matter!)  Incidentally, the
union function then illustrates Brian's point beautifully:
	union (S xs) (S ys) = S (merge xs ys)
The Ord constraint needed by merge can be satisfied from either the (S xs) or the (S ys) -- and they'd better be
the same Ord implementation!

Thirdly, and most significantly, it's quite hard to *exclude* examples like 'Problem' if we allow general
equality constraints (which we now do).  For example,
	Problem2 :: forall a b. (Num b, a~b) => T a
Here Num constrains an "existential" variable... but not really, because the (a~b) constraint makes it
equal to 'a'.  In general, it might not be precisely equal but somehow connected:
	Problem3 : forall a b. (Num b, F a ~ G b) => T a
where F and G are type functions.  So it's getting complicated.  Since Haskell *does* have global instances,
I decided not to try to find the bottom of this particular tarpit, and instead adopted the simple story: you
can give a data constructor an arbitrary set of constraints.  GADTs are merely a special case, in which the
type constraints are all equalities. 

All that said, I agree that the ice is thin here. For example, if you allow overlapping instances (which some
people like) then I think you could cook up an example in which the choice mattered.  So I am not arguing that
(Continue reading)

Permalink | Reply | 2 comments |
headers
Derek Dreyer | 7 Oct 2009 16:16
Favicon

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi, Brian.

> Thanks for pointing out that the compiler could just reject this clause: perhaps this would be an
acceptable penalty to pay for the advantages of having scoped instances. However there are situations
where it would not be so clear what the compiler should do eg:
>
>    bar :: forall a. G a -> (a, Int)
>    bar (Problem x) = (x + x, 1 + 2)
>    bar (Ok _)      = ((), 0)
>
> In the expression (x + x, 1 + 2), what instance should the compiler use for (1 + 2)? Since (bar) is
polymorphic, the compiler, when compiling (bar), has no way of knowing whether or not the match against
(Problem x) is going to introduce a Num Int dictionary.

I think you're getting confused about the problem Karl pointed out
with the original example (at least why it would be a problem in the
modular type class setting).

The problem was *not* that by unpacking the GADT arguments you were
introducing instances into scope that overlapped with Num Int.  The
problem was that you were unpacking *two* arguments of type G a, which
introduced two overlapping instances of Num a.

The "bar" example above is fine, because you're just unpacking one
argument of type G a, and since "a" is a freshly bound type variable,
it's fine to introduce an instance of Num a (as it can't overlap with
anything else).
(Continue reading)

Permalink | Reply | 1 comment |
headers
Brian Hulley | 7 Oct 2009 23:28

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Simon Peyton-Jones wrote:
> 
> The ability to have a data constructor capture a constraint
> of a *non-existential* type variable is newish in GHC.  I added it
> for several reasons.  Firstly, it is more uniform.  It's great to be
> able to say "You can give a constructor any old type, with
> arbitrary constraints".  Secondly, it's useful,  You can have,
> the constructor for (Set a) capturing the (Ord a) constraint, eg
>    data Set a where
>       S :: forall a. Ord a => [a]
> so that union can have type union :: Set a -> Set a -> Set a.
> (Empty set is another matter!)  Incidentally, the union function
> then illustrates Brian's point beautifully:
> 	union (S xs) (S ys) = S (merge xs ys)
> The Ord constraint needed by merge can be satisfied from either
> the (S xs) or the (S ys) -- and they'd better be the same Ord implementation!
> 

Actually even if we go back to plain Haskell 98 and consider the original types for the functions in Data.Set
we can see that none of the types would be sufficient to describe the parameter requirements in a modular setting:

    data Set a = Set [a] -- example implementation

    insert :: Ord a => a -> Set a -> Set a

    union  :: Ord a => Set a -> Set a -> Set a

The problem is, for these type signatures to be correct in the sense that they would force the programmer to
(Continue reading)

Permalink | Reply | 1 comment |
headers
Brian Hulley | 7 Oct 2009 23:41

Re: A show-stopping problem for modular type classes?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

[Apologies if you've received this twice - I sent it first from the wrong address]

Brian Hulley wrote:
> From this angle it is then easy to see that far from regarding the 
> global nature of Haskell typeclass instances as a minor inconvenience 
> to be circumvented by lexical scoping or some other mechanism, it is 
> in fact the central core of the concept itself!

For some reason my email program made it look as if the above paragraph, 
which I wrote, was quoted from Simon's post. Apologies for the confusion,

Brian.
Permalink | Reply | 0 comments |

Gmane