The dependent types in ATS are not the kind of full spectrum dependent types
as formulated in Martin-Lof's constructive type theory. I now refer to the
dependent
types in ATS as DML-style dependent types, which I first formulated in
Dependent ML
(DML), a language I designed and implemented as a
Exciting! I can't wait! :D
On Thursday, June 3, 2021 at 6:31:11 PM UTC-4 gmhwxi wrote:
>
> Hi, there,
>
> I wish I could announce that ATS is ready. But it is not.
>
> I had actually gotten stuck for quite some time in the middle of
> implementing a type-checker for ATS3 (that supports both line
No problem. ✌😊
On Thu, Jun 3, 2021, 6:36 PM David Smith wrote:
> Yes! stropt seems to be exactly what I want. Thank you!
>
> d4v3y_5c0n3s schrieb am Donnerstag, 3. Juni 2021 um 22:23:57 UTC:
>
>> I would suggest either trying the "stropt" type or the "Option_vt" type.
>> Would you mind sharing a
Yes! stropt seems to be exactly what I want. Thank you!
d4v3y_5c0n3s schrieb am Donnerstag, 3. Juni 2021 um 22:23:57 UTC:
> I would suggest either trying the "stropt" type or the "Option_vt" type.
> Would you mind sharing a snippet of code, so that we could get a better
> understanding of what
I'd suggest using an external function/value with dependent types that tell
ATS the "sort" of the pointer is "agz" (arguements greater than zero.)
I'll try to put together an example.
On Thu, Jun 3, 2021, 6:15 PM David Smith wrote:
>
> When dealing with memory mapped IO, is there a neat way to a
Well, I believe that you could just call the praxi in the body of your "or"
function just like you would with any function. I don't have the ability
to test this at the moment, but later I will try to show you an example of
what I mean.
On Thu, Jun 3, 2021, 6:26 PM David Smith wrote:
> Ah, that
Hi, there,
I wish I could announce that ATS is ready. But it is not.
I had actually gotten stuck for quite some time in the middle of
implementing a type-checker for ATS3 (that supports both linear
types and dependent types). It is some work I did in the last few
days that has unstuck me. Hopefu
Ah, that sounds like a pretty neat solution.
How exactly do I make ATS know that my function that does the or-ing should
make use of that proof?
d4v3y_5c0n3s schrieb am Samstag, 29. Mai 2021 um 15:39:37 UTC:
> Hey David, have you tried using the "praxi" syntax? It allows you to
> define an ax
I would suggest either trying the "stropt" type or the "Option_vt" type.
Would you mind sharing a snippet of code, so that we could get a better
understanding of what you are trying to do?
On Thu, Jun 3, 2021, 6:00 PM David Smith wrote:
> I'm trying to wrap a library that has a function that tak
When dealing with memory mapped IO, is there a neat way to axiomatically
say "there is something at address 0x12345678?
At the moment I'm using a C macro that just returns the address, and then
have an at-view in the ATS type signature, though I'd prefer to somehow
treat that as global, if onl
I'm trying to wrap a library that has a function that takes a `char *`, and
optionally NULL.
I tried strptr, string, and other random types I found in the prelude. Now
I'm trying to pass NULL (using `the_null_ptr`; great name btw), and I'm
getting type errors.
Which string should I use here, a
11 matches
Mail list logo
