Bigos
2/21/2016 2:29:00 PM
On 21/02/16 11:16, Rob Warnock wrote:
>
> Without delving into the details of your examples, one thing
> stood out for me: It looks like you're trying to get the
> Common Lisp type declaration mechanism to do something it
> was never intended to do. That is, in Common Lisp a type
> declaration is not a request that the implementation *enforce*
> your types, but rather a promise by you *to* the implementation
> that the data mentioned will always be of the declared type(s)!
>
> Said another way, instead of the "check me" of other languages,
> in Common Lisp a type declaration means "trust me"!! But
> you'd better not ever lie to the compiler about your types.
> As CLHS 3.3 "Declarations" specifically warns:
>
> The consequences are undefined if a program
> violates a declaration or a proclamation.
>
> +---------------
> | Would I use my spare time better trying to learn some
> | proving tools like ACL2?
> +---------------
>
> That might be helpful...
>
>
I'm NOT trying to enforce types. Having load/compile time warning is
good enough.
I'm my example at the top of the thread SBCL does exactly that.
I guess one could write a tool that would generate tests that would
result in the same informations as compile time type checking in other
languages.
Here comes my second part of the question. how hard it is to use ACL2
for that?
Haskellers are promising a lot with their language, but I find their
almost mathematical notation counter intuitive. I love parentheses, feel
like fish in the water when using Emacs and paredit.
I don't know enough Haskell to verify their claims. On few occasions I
have ran into problems where I badly needed type based optimisations to
finish my code running within allocated time. But that can be done with
type declarations I already know.
Haskellers seem to indicate that they can use types to almost prove
correctness of their programs. Am I wasting time trying to investigate
this path? What should I do?