3 ms·

You can't, not with Haskell. (Maybe you can, I don't know, with some really insane extensions and type-level programming. It wouldn't be nice.) Haskell's app

• js8 11y ago
  I agree that you can probably do that with dependent-types, I am just wondering if there is a way to do stuff like that in more simpler formalism, similar to untyped lambda calculus. I mean, in untyped lambda calculus you start with simple objects that are fully specified and you compose them to get more complex objects. I think one should be able to do the "opposite" thing, i.e. start with potentially complicated objects and restrict those down by adding relational conditions on them. So I am looking for some (minimalistic) formalism to do that, something like "lambda calculus in reverse". In classic Lisp, there were operators CAR, CDR and EQ which let you introspect any lambda expression. So maybe there should exist a formalism having these decompositional operators as primitives..
  • theseoafs 11y ago
    You already know it: the way you do this is with a homoiconic language. I don't know of any "formalisms" of homoiconic languages, but there's always Scheme. I don't know why this idea is relevant though. If where you're going with this is "you can write code to take in a monad instance as an input syntax tree and verify it satisfies the laws", then I assure you that's impossible in the general case.