[lnkForumImage]
TotalShareware - Download Free Software

Confronta i prezzi di migliaia di prodotti.
Asp Forum
 Home | Login | Register | Search 


 

Forums >

comp.lang.lisp

sbcl type declarations and checking

Bigos

2/21/2016

What is the best way of declaring types in SBCL?

I have tried two different approaches a history of this file can show:

https://goo...

To my surprise example from:

http://ahungry.com/blog/2015-07-10-Type-Safety-and-Lack-Th...

with haskell style declaration does not give warning when I give
incorrect result type. Was it prepared with different implementation?


In SBCL following seems to work:

(declaim (ftype (function (integer integer) (symbol))
my-mod))

(defun my-mod (a b) ;declaring incorrect results gives compile error
(mod a b))

When I break the declaration and declare result as symbol I get expected
error.

Is there any value in trying to use type checking with CL?

I know that different implementations handle matter of type checking
differently and there is no standard. But I wonder if it is worth to
look with jealousy at Haskellers and try to copy their types.

On one hand I seem to see the point of type checking when handling
binary files. Also some type declarations can greatly increase running
speed and compile code comparable to C compilers output.

But am I wasting my time going down this path? Are there Lisp code
analysis tools that could do the same job without resorting to type
declarations?

Would I use my spare time better trying to learn some proving tools like
ACL2?
21 Answers

Matthew Carter

2/21/2016 3:39:00 AM

0

Bigos <ruby.object@googlemail.com> writes:

> What is the best way of declaring types in SBCL?
>
> I have tried two different approaches a history of this file can show:
>
> https://goo...
>
> To my surprise example from:
>
> http://a.../blog/2015-07-10-Type-Safety-and-Lack-Th...
>
> with haskell style declaration does not give warning when I give
> incorrect result type. Was it prepared with different implementation?
>
>
> In SBCL following seems to work:
>
> (declaim (ftype (function (integer integer) (symbol))
> my-mod))
>
> (defun my-mod (a b) ;declaring incorrect results gives compile error
> (mod a b))
>
> When I break the declaration and declare result as symbol I get
> expected error.
>
> Is there any value in trying to use type checking with CL?
>
> I know that different implementations handle matter of type checking
> differently and there is no standard. But I wonder if it is worth to
> look with jealousy at Haskellers and try to copy their types.
>
> On one hand I seem to see the point of type checking when handling
> binary files. Also some type declarations can greatly increase running
> speed and compile code comparable to C compilers output.
>
> But am I wasting my time going down this path? Are there Lisp code
> analysis tools that could do the same job without resorting to type
> declarations?
>
> Would I use my spare time better trying to learn some proving tools
> like ACL2?

It doesn't give a warning when you give an incorrect result type, as in
you pass in something like:

(Æ?â?? stringer (string â?? int) "dog" â?? 1 "cat" â?? 2)

Letting you know that "int" isn't a valid type? While:

(Æ?â?? numberer (int â?? string) 1 â?? "dog" 2 â?? "cat")

would?

Because I think it works fine at the moment if you load it up with the
following:

(ql:quickload :glyphs)
(use-package :glyphs)
(in-readtable glyphx:syntax)

But definitely let me know if not.

--
Matthew Carter (m@ahungry.com)
http://a...

Matthew Carter

2/21/2016 3:54:00 AM

0

Matthew Carter <m@ahungry.com> writes:

> Bigos <ruby.object@googlemail.com> writes:
>
>> What is the best way of declaring types in SBCL?
>>
>> I have tried two different approaches a history of this file can show:
>>
>> https://goo...
>>
>> To my surprise example from:
>>
>> http://a.../blog/2015-07-10-Type-Safety-and-Lack-Th...
>>
>> with haskell style declaration does not give warning when I give
>> incorrect result type. Was it prepared with different implementation?
>>
>
> It doesn't give a warning when you give an incorrect result type, as in
> you pass in something like:
>
> (Æ?â?? stringer (string â?? int) "dog" â?? 1 "cat" â?? 2)
>
> Letting you know that "int" isn't a valid type? While:
>
> (Æ?â?? numberer (int â?? string) 1 â?? "dog" 2 â?? "cat")
>
> would?
>
> Because I think it works fine at the moment if you load it up with the
> following:
>
> (ql:quickload :glyphs)
> (use-package :glyphs)
> (in-readtable glyphx:syntax)
>
> But definitely let me know if not.

Sorry, if the last part wasn't clear - it won't alert if a type doesn't
exist in the function definition (non-existent type), but it should be
alerting if you set up a typed function and then attempt to call the
typed function with a type that it knows will return a different type
within another function definition.

--
Matthew Carter (m@ahungry.com)
http://a...

Bigos

2/21/2016 9:21:00 AM

0

On 21/02/16 03:54, Matthew Carter wrote:
> Matthew Carter <m@ahungry.com> writes:
>
>
> Sorry, if the last part wasn't clear - it won't alert if a type doesn't
> exist in the function definition (non-existent type), but it should be
> alerting if you set up a typed function and then attempt to call the
> typed function with a type that it knows will return a different type
> within another function definition.
>
It's morning now. I have to go somewhere. I will provide code example
in the afternoon.

rpw3

2/21/2016 11:17:00 AM

0

Bigos <ruby.object@googlemail.com> wrote:
+---------------
| What is the best way of declaring types in SBCL?
....
| Is there any value in trying to use type checking with CL?
|
| I know that different implementations handle matter of type checking
| differently and there is no standard. But I wonder if it is worth to
| look with jealousy at Haskellers and try to copy their types.
....
| But am I wasting my time going down this path? Are there Lisp code
| analysis tools that could do the same job without resorting to type
| declarations?
+---------------

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...


-Rob

-----
Rob Warnock <rpw3@rpw3.org>
627 26th Avenue <http://rpw...
San Mateo, CA 94403

Bigos

2/21/2016 2:29:00 PM

0

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?


Pascal Costanza

2/21/2016 2:36:00 PM

0

On 21/02/2016 15:28, Bigos wrote:
> 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.

Common Lisp implementations are not required to give you such warnings.
Some implementations, especially SBCL, are pretty good at that, but you
still cannot rely on it. If the compiler doesn't give you a warning,
that doesn't mean there is no problem. The warnings are merely an aid,
without any systematic guarantees that you will actually get them if
something is problematic.

> Here comes my second part of the question. how hard it is to use ACL2
> for that?

ACL2 is very different from CL. It's best to just try it, and you'll see.

The purpose of ACL2 is not to be a general-purpose programming language,
so it may not be your best choice. If you want to have some form of
static typing, it may be better to try other statically typed Lisp
dialects, like for example Typed Racket, or so.

> 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?

Only you yourself can answer that question.

Pascal

--
My website: http:/...
Common Lisp Document Repository: http://cdr.eu...
Closer to MOP & ContextL: http://common-lisp.net/proje...
The views expressed are my own, and not those of my employer.

Bigos

2/21/2016 3:54:00 PM

0

On 21/02/16 14:36, Pascal Costanza wrote:
> On 21/02/2016 15:28, Bigos wrote:
>> 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.
>
> Common Lisp implementations are not required to give you such warnings.
> Some implementations, especially SBCL, are pretty good at that, but you
> still cannot rely on it. If the compiler doesn't give you a warning,
> that doesn't mean there is no problem. The warnings are merely an aid,
> without any systematic guarantees that you will actually get them if
> something is problematic.
>
>> Here comes my second part of the question. how hard it is to use ACL2
>> for that?
>
> ACL2 is very different from CL. It's best to just try it, and you'll see.
>
> The purpose of ACL2 is not to be a general-purpose programming language,
> so it may not be your best choice. If you want to have some form of
> static typing, it may be better to try other statically typed Lisp
> dialects, like for example Typed Racket, or so.
>
>> 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?
>
> Only you yourself can answer that question.
>
> Pascal
>

I saw a blog written by a Racket programmer saying that you can't just
convert untyped Racket to typed one. You are better off starting from
scratch writing typed version. Perhaps I would have the same problems
with Common Lisp.

If I can't rely on SBCL's type warnings then perhaps ACL2 of similar
tool might be the only way to go.

https://github.com/acl2/acl2/tree/master/books/proje...

Pascal Costanza

2/21/2016 4:15:00 PM

0

On 21/02/2016 16:53, Bigos wrote:
> I saw a blog written by a Racket programmer saying that you can't just
> convert untyped Racket to typed one. You are better off starting from
> scratch writing typed version. Perhaps I would have the same problems
> with Common Lisp.
>
> If I can't rely on SBCL's type warnings then perhaps ACL2 of similar
> tool might be the only way to go.
>
> https://github.com/acl2/acl2/tree/master/books/proje...

Moving from Common Lisp to ACL2 will be even harder than moving from
Racket to Typed Racket, because the language in ACL2 is even further
away from Common Lisp. ACL2 is not a general-purpose language, you will
have to write code in a purely applicative style and prove to the system
on every step that your functions terminate, etc. If your expectation is
that this is anything like programming in CL, you will have to change
you expectations dramatically. I don't know what your goals are, but
it's very likely that it won't make sense unless you have very
specialized needs.


Pascal

--
My website: http:/...
Common Lisp Document Repository: http://cdr.eu...
Closer to MOP & ContextL: http://common-lisp.net/proje...
The views expressed are my own, and not those of my employer.

Paul Wallich

2/21/2016 6:56:00 PM

0

On 2/21/16 10:53 AM, Bigos wrote:
> On 21/02/16 14:36, Pascal Costanza wrote:
>> On 21/02/2016 15:28, Bigos wrote:
>>> 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.
>>
>> Common Lisp implementations are not required to give you such warnings.
>> Some implementations, especially SBCL, are pretty good at that, but you
>> still cannot rely on it. If the compiler doesn't give you a warning,
>> that doesn't mean there is no problem. The warnings are merely an aid,
>> without any systematic guarantees that you will actually get them if
>> something is problematic.
>>
>>> Here comes my second part of the question. how hard it is to use ACL2
>>> for that?
>>
>> ACL2 is very different from CL. It's best to just try it, and you'll see.
>>
>> The purpose of ACL2 is not to be a general-purpose programming language,
>> so it may not be your best choice. If you want to have some form of
>> static typing, it may be better to try other statically typed Lisp
>> dialects, like for example Typed Racket, or so.
>>
>>> 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?
>>
>> Only you yourself can answer that question.
>>
>> Pascal
>>
>
> I saw a blog written by a Racket programmer saying that you can't just
> convert untyped Racket to typed one. You are better off starting from
> scratch writing typed version. Perhaps I would have the same problems
> with Common Lisp.
>
> If I can't rely on SBCL's type warnings then perhaps ACL2 of similar
> tool might be the only way to go.
>
> https://github.com/acl2/acl2/tree/master/books/proje...

Is there a reason that you can't easily put explicit type
assertions/checks into your code, perhaps semi-automatically? CL won't
automatically check types for you, but if you ask it "Is the thing I'm
referring to of such-and-such a type" it will generally be happy to answer.

paul

Madhu

2/22/2016 1:29:00 PM

0


"Unfortunately, Common Lisp is the standard, in more ways than one.
Thousands of person-hours are devoted to implementing, maintaining, and
documenting it, whereas T is the work of a handful of eccentrics. Like
Scheme, its parent, people who like T become fanatically devoted to it,
but they have to put up with a lot, including a compiler that works
correctly and effciently only for stylistically fashionable code. NISP
is an effort to survive in both these worlds.[...]"

-- Drew McDermott, NISP Manual 1988?
http://cs-www.cs.yale.edu/homes/dvm/papers/n...

[Chapter 4 "NISP Type System" may be of interest to some recent posters]