Thanks again for your comments! They are absolutely very helpful!
I feel I'm trying to free-my-mind here; still working on losing the idea
that type-checking is magic done by the system/language, and instead
something the programmer can use at will, and creatively, and in unexpected
ways. Not only to check that code is not wrong, but to drive progression in
a multi-stage evaluation; choose among specific implementations that are
doing work that is conceptually the same, but implementation-wise
different, reflect the state of the evaluation and possible interactions as
user UI on a web page etc etc.
Regards /Henning
On Thu, Apr 25, 2019 at 2:55 AM Ben Sima <b...@bsima.me> wrote:
> Henning Sato von Rosen <henning.von.ro...@gmail.com> writes:
>
> > Sorry if I'm wrong here, but I'm not sure we are talking about the same
> > data-type; I'm not referring to the Rich's examples with Maybe, but his
> > examples with records/maps, where some fields may or may not be present.
>
> Right, and in most other type systems, the only way to indicate
> field presence is with a Maybe type:
>
> data MyData = MyData
> { oneField = Maybe Int
> , twoField = Maybe String
> }
>
> So to convey that these fields don't exist, we have to explicitly say
> "Nothing":
>
> instance Monoid MyData where
> mempty = MyData { oneField = Nothing, twoField = Nothing }
>
> which, in GHC, is known and enforced at compile-time. In lisp, if a
> field isn't present in a record, you get nil:
>
> (get {:a 1} :b) ;;=> nil
>
> but this is only decidable at runtime. So core.spec takes this "tooling"
> around typechecking and exposes it to the user so they could do program
> analysis (like seeing what functions are applicable, etc) at
> runtime. Racket's contract system does the same, afaik.
>
> Presumably you could implement a Hindley-Milner type system using
> core.spec. That would be cool. E.g. Shen is a lisp with a type system in
> which you could implement HM in just a few pages of code.
>
> Not sure if this is helpful, hope you get something out of it.
>
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clojure@googlegroups.com
Note that posts from new members are moderated - please be patient with your
first post.
To unsubscribe from this group, send email to
clojure+unsubscr...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en
---
You received this message because you are subscribed to the Google Groups
"Clojure" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to clojure+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
