Re: [Haskell-cafe] modules as implicit data structures

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 のメール:

Thank you everyone, these are some very interesting pointers to explore!

Petr

čt 6. 9. 2018 v 15:01 odesílatel Sven Panne napsal: Am Do., 6. Sep. 2018 um 11:43 Uhr schrieb Petr Pudlák : [...] 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@gmail.com 筑波大学数理物質科学研究科 数学専攻 博士後期課程三年 ----------------------------------------------