[Agda] Exports example? Making ADT constructors private?

[Evan Czaplicki]

That makes sense, thank you :) Do you like doing things that way? Like,
more than the big list at the top of the file?

P.S. Agda has already influenced Elm :) I've had my eye on parameterized
modules and implicit arguments for a while now, and I plan features knowing
that I'm probably adding these someday :) Also, I have not written tons of
Agda yet, but I am constantly impressed by how it gracefully it extends and
simplifies syntax and semantics.


On Sun, Oct 6, 2013 at 7:21 AM, Brian McKenna <brian at brianmckenna.org>wrote:

> Hi Evan,
>
> Awesome to see you on the Agda list. I hope it'll influence Elm.
>
> The way I know how to do this is like so:
>
>     module Movement where
>
>     private
>       data Direction' : Set0 where
>            Up : Direction'
>            Down : Direction'
>
>     open Direction' public hiding (Down)
>
>     Direction : Set0
>     Direction = Direction'
>
> You can probably see what's happening with the private block and the
> open import. The interesting thing is that (as far as I can tell) the
> open import doesn't re-export the Direction' type, therefore we have
> to do that ourselves.
>
> Does that make sense?
>
> Thanks,
> Brian McKenna
>
> On 5 October 2013 20:30, Evan Czaplicki <evancz at gmail.com> wrote:
> > How would I make the Up constructor private in the following module?
> (Just
> > Up, but not Down)
> >
> > module Movement where
> >
> > data Direction where
> >     Up : Direction
> >     Down : Direction
> >
> > I know there is a "private" annotation, but I'm not sure where to put it
> for
> > ADTs. Also, is "private" the primary way to mark what gets exported and
> what
> > does not? (i.e. is the Haskell way of doing things totally done away
> with?)
> >
> > Thank you!
> > Evan
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131009/c325d03c/attachment.html