[Haskell-cafe] modules as implicit data structures

Hiromi ISHII konn.jinro at gmail.com
Tue Sep 11 07:05:39 UTC 2018

Hi Petr,

I think Agda's module system is something similar to your conception.
In Agda, you can treat modules and records interchangably.

> 2018/09/11 1:16、Petr Pudlák <petr.mvd at gmail.com>のメール:
> Thank you everyone, these are some very interesting pointers to explore!
> Petr
> čt 6. 9. 2018 v 15:01 odesílatel Sven Panne <svenpanne at gmail.com> napsal:
> Am Do., 6. Sep. 2018 um 11:43 Uhr schrieb Petr Pudlák <petr.mvd at gmail.com>:
> [...] Has some language explored this idea of making modules explicit as language-level objects? It seems that there could be some interesting possibilities, such as: [...]
> You might want to have a look at Standard ML's signatures, structures and functors, they are probably what you're thinking about.
> Cheers,
>    S.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

----- 石井 大海 ---------------------------
konn.jinro at gmail.com
数学専攻 博士後期課程三年

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: Message signed with OpenPGP
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180911/ab5b9697/attachment.sig>

More information about the Haskell-Cafe mailing list