search

bryanedds / Sedela

The official repo for Sedela, the Semantic Design Lenguage.
MIT License
2 stars 1 forks source link

Laws using Dependent Types #1

Open bryanedds opened 5 years ago

bryanedds commented 5 years ago

@iitalics proposes an alternative to Type Class Morphisms with Dependent Types using Agda here -

https://gist.github.com/iitalics/e15e578947bf0f77970e3eda6de839e6

What does this mean for Sedela's design?

bryanedds commented 5 years ago

Redex tutorial / reference located here - http://docs.racket-lang.org/redex/

bryanedds commented 5 years ago

Oh, and the original Type Class Morphisms paper is here - http://conal.net/papers/type-class-morphisms/type-class-morphisms-long.pdf

bryanedds commented 5 years ago

While this approach is a fine curiosity, I don't think this approach has any implications for Sedela in practice. Like HM types are a sweet-spot for general-purpose programming languages, TCMs are a sweet spot for semantic design, IMO. Also like types for GPLs, Dependent Types are overkill.

The alternative approach is still worth keeping in mind and reflecting upon as we proceed, however.

bryanedds commented 4 years ago

UPDATE:

A workmate of mine disagrees with my analysis that typeclasses are the best representation. He argues that rather than the typeclasses, it is the laws that matter most. I am starting to see the wisdom in his opposing analysis.

Perhaps the approach by @iitalics has more promising implications that I had at first concluded. Perhaps Agda - or something like it that can express laws directly - should be our functional modeling language of choice.

bryanedds commented 4 years ago

One interesting thought is the idea that any laws or valid combination of laws should be representable as a typeclass / category. So while Sedela cannot express laws directly, it can represent them in any valid combination. Is this not sufficient?