No, a proof is not a type. A proof is a total program (that is pure and
terminating).
On Friday, March 22, 2019 at 1:55:17 PM UTC-4, Yannick Duchêne wrote:
>
> Within ATS, is it correct to say a proof is usually a dependant type?
> (whose value just get discarded from the generated program).
>
Sounds like I have to fix atspkg :p
If you want to use the monads package with npm + Makefiles, I suppose I
could upload to npm (it might even be a good idea given the permanence
of packages there).
As an aside: I suspect that what makes IO so nice in the context of
Haskell is that you get the
On Friday, March 22, 2019 at 2:49:29 PM UTC-4, Brandon Barker wrote:
>
> Hey Artyom,
>
> Thanks for the very interesting analysis and response.
>
> On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <
> artyom.shalkha...@gmail.com> wrote:
>
>> Hi Brandon,
>>
>> This is a very lively discussion,
