Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
Coming from First class instances, ignoring status quo, if we were to design typeclasses from ground up, we could drop class syntax altogether in favour of e.g. codata syntax:
codata Foo a where
foo :: a
bar :: Int
(dual to GADTSyntax), provide ability to add fundeps and associated families to datatypes, and recover DatatypeContexts syntax, just changed to implement GADT-like dictionary-carrying behaviour :smiley:
your codata = agda record?
what's the difference between that and haskell records as they are today, except from
Well, I guess we could drop traditional data syntax altogether - mixing of types and data constructors seems to be confusing for newcomers and GADTSyntax provides superset of it's functionality
Compared to record inside of GADTSyntax, it would be more convenient to write and modify
(in case of records)
And would basically work as a substitute for class syntax in language where there's no distinction between Constraint and Type