help from the community?

[Malcolm Wallace]

isaac jones <ijones at galois.com> wrote:

> > http://hackage.haskell.org/trac/haskell-prime/ticket/57
> 
> Does anyone have any feedback on this work?

Yes, here are my thoughts.

> PROPOSAL: adopt GHC's convention and treat 'forall' specially in types
> but allow it to be used in value declarations.

Agree.

> [ scheme  = 'forall' tvars '.' opt_ctxt type ]
> The non-terminal 'tvars' is a sequence of type variables that are
> separated by blank spaces. We have a choice if we should allow empty
> quantifier sequences.
> PROPOSAL: be liberal:
>   * allow empty quantifier lists
>   * allow variables that are not mentioned in the body of a type (but warn)
>   * allow predicates that do not mention quantified variables (but warn?)

I cannot see how an empty list of tyvars is useful or desirable in
practice:
    data Foo = Foo (forall . Int)
is equivalent to just
    data Foo = Foo Int
so why bother to permit the former?  It probably indicates some error in
the thinking of the programmer, so the compiler should bring it to her
attention.

On the other hand, I can imagine a use for phantom type variables in the
quantifier (especially if they occur in multi-parameter predicates, but
not in the type).  So I think accepting them with a warning is
reasonable.

I can also imagine predicates that do not mention locally-quantified
variables - the assumption must be that they mention variables bound on
the LHS of the datatype decl instead?  e.g. the Show predicate here:

    data Foo a b = Foo a b
                 | Bar (forall c . (Show b, Relation b c) => (b,c))

Hmm, maybe a simpler version of this example would illustrate what you
mean by the proposal (first of the three bullets) to allow an empty
quantifier list:

    data Foo a b = Foo a b
                 | Bar (forall . Show b => b)

In which case, does this even count as a polymorphic component at all?
Is it not rather GADT-like instead?

    data Foo a b where
      Foo :: a -> b -> Foo a b
      Bar :: Show b => b -> Foo a b

> Strict Fields: Where should we place the '!'?
> PROPOSAL: before a schema and the schema has to be in parens.

Seems the only reasonable choice.

> Labelled Fields.
> PROPOSAL: Use syntactic equivalence modulo
>   * alpha renaming
>   * order/repetition of predicates (i.e. compare predicates as sets)

Seems OK.  Using entailment looks like it would permit a far more
obfuscated programming style, without adding any useful functionality.

> Constructor that have polymorphic components cannot appear in the
> program without values for their polymorphic fields.

I didn't fully understand this requirement.  If Haskell-prime gets
rank-2 or rank-n types, then do we need to restrict constructors in this
way?

> We do not allow nested patterns on fields that have polymorphic types.

Yes, agree.

Regards,
    Malcolm