I am a bit surprised. It did not work. It works now because of a recent
change I made on checking type equality (my guess).
On Wednesday, May 2, 2018 at 12:17:26 AM UTC-4, Steinway Wu wrote:
>
> I actually just tried it, and it works with `[n:nat] List (a, n)`. See
> https://glot.io/snippets/f0n
I actually just tried it, and it works with `[n:nat] List (a, n)`. See
https://glot.io/snippets/f0nf39m7lk.
On Tuesday, May 1, 2018 at 11:59:32 PM UTC-4, Steinway Wu wrote:
>
> Oh I see. But anyway, here's a monad type class. Just for the record.
>
> https://glot.io/snippets/f0nejek645
>
>
> On
Oh I see. But anyway, here's a monad type class. Just for the record.
https://glot.io/snippets/f0nejek645
On Tuesday, May 1, 2018 at 11:27:29 PM UTC-4, gmhwxi wrote:
>
>
> This approach can only handle simple type constructors like list and maybe.
> It would not handle List defined as follows:
wrote:
>>
>>
>> If we box everything, then implementing functors (as is defined in
>> Haskell) is straightforward
>> in ATS. However, for performance, one may not want to box everything. I
>> sketched a template-based
>> implementation for functors as follows:
h 29, 2017 at 10:38:00 AM UTC-4, gmhwxi wrote:
>
>
> If we box everything, then implementing functors (as is defined in
> Haskell) is straightforward
> in ATS. However, for performance, one may not want to box everything. I
> sketched a template-based
> implementation for f
If you use t0ype, the compiler cannot figure out the size of r, causing a
compilation error.
Sent from my T-Mobile 4G LTE device
-- Original message--
*From: *August Alm
*Date: *Wed, Apr 5, 2017 3:18 PM
*To: *ats-lang-users;
*Subject:*Re: Template-based implementation for functors
gt;>>>>>>>
>>>>>>>>>>> When mapM_list_vt$aux is compiled. {m:fvtype} is not
>>>>>>>>>>> instantiated.
>>>>>>>>>>> Only template parameters are instantiated. This is a big
>>>>>>>> incorrect.
>>>>>>>>>>> The code should have compiled. I will see if I can figure out
>>>>>>>>>>> the cause for this bug.
>>>>>>>>>>>
>>>>>>>>>>>
gt;>> let implement mapM_list_vt$fopr(x) = fopr(x)
>>>>>>>>>>> in mapM_list_vt$aux{m}{n}(pfm| xs) end
>>>>>>>>>>>
>>>>>>>>>>> So the implementation of mapM_list_vt$fopr cannot be used for
>>>>>&g
gt;
>>>>>>>>>>> Great! But ...What just happened, what's the lesson I should
>>>>>>>>>>> take away?
>>>>>>>>>>>
>>>>>>>>>&
ou change the body of mapM_list_vt_fun as follows:
>>>>>>>>>>>
>>>>>>>>>>> let
>>>>>>>>>>> implement(a,s)
>>>>>>>>>>
>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> On Thu, Mar 30, 2017 at 5:11 PM, August Alm
>>>>>>>>>> wrote:
>>>>>>>>>>
>>>>>>>>>>> I think the
t;>>>>>>>>
>>>>>>>>>> or
>>>>>>>>>>
>>>>>>>>>> extern fun{m_name: type}{a, b: vt0ype}
>>>>>>>>>> {m: fvtype}
>>>>>>>>>> mapM_list_vt$fopr(MON
> Is there a way to coerce the typechecking in situations like this?
>>>>>>>>>
>>>>>>>>> Best,
>>>>>>>>> August
>>>>>>>>>
>>>>>>>>> Den torsdag 30 mars 2017 kl. 18:
se:
>>>>>>>>>
>>>>>>>>> val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))
>>>>>>>>>
>>>>>>>>> changes to
>>>>>>>>>
>>>>>>>>> val xs =
>>>> val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))
>>>>>>>>>
>>>>>>>>> changes to
>>>>>>>>>
>>>>>>>>> val xs = $list_vt{int_vt}(I(1), I(2), I(3))
>>>>>>>>>
>>&
hing could remove the need
>>>>>>>>>>> for the user to explicitly define "extern praxis FUNCTOR_f_elim"
>>>>>>>>>>> and
>>>>>>>>>>> "abstype f_name" for each functo
gt;>>>
>>>>>>>>> Something can definitely done along this line. At some point in
>>>>>>>>> the past,
>>>>>>>>> I was even contemplating some kind of support for automatically
>>>>>>>>>
t;>> https://glot.io/snippets/eoh28sd2p4
>>>>>>>>>>
>>>>>>>>>> Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi:
>>>>>>>>>>>
>>>>>>>>>>> I see. Maybe a clever macro or
omething could remove the need
>>>>>>>>>>> for the user to explicitly define "extern praxis FUNCTOR_f_elim"
>>>>>>>>>>> and
>>>>>>>>>>> "abstype f_name" for each functor ins
gt;>>>>
>>>>>>>>>
>>>>>>>>> Something can definitely done along this line. At some point in
>>>>>>>>> the past,
>>>>>>>>> I was even contemplating some kind of support for automati
d right away because I wanted to see more use
>>>>>>>> cases involving
>>>>>>>> concepts from category theory.
>>>>>>>>
>>>>>>>> On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote:
>
t; cases involving
>>>>>>> concepts from category theory.
>>>>>>>
>>>>>>> On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote:
>>>>>>>>
>>>>>>>> Den torsdag 30 mars 2017
gt; synthesizing
>>>>>>>> proofs of certain props. Kind of like inferring dictionaries for
>>>>>>>> type classes.
>>>>>>>>
>>>>>>>> I did not go forward right away because I wanted to see more use
>
t;
>>>>>>> On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm wrote:
>>>>>>>>
>>>>>>>> Den torsdag 30 mars 2017 kl. 04:22:08 UTC+2 skrev gmhwxi:
>>>>>>>> > Unfortunately, using a type functio
t;> I did not go forward right away because I wanted to see more use
>>>>>>> cases involving
>>>>>>> concepts from category theory.
>>>>>>>
>>>>>>> On Thursday, March 30, 2017 at 4:37:47 AM UTC-4, August Alm
AM UTC-4, August Alm wrote:
>>>>>>>
>>>>>>> Den torsdag 30 mars 2017 kl. 04:22:08 UTC+2 skrev gmhwxi:
>>>>>>> > Unfortunately, using a type function (of the sort ftype or fvtype)
>>>>>>> as a
>>>>
>>>>> > Unfortunately, using a type function (of the sort ftype or fvtype)
>>>>>>> as a
>>>>>>> > template argument is currently not supported. That is why I used a
>>>>>>> "name"
>>>>>>
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>>>>>> >
>>>>>> > On Wednesday, March 29, 2017 at 6:36:02 PM UTC-4, August Alm wrote:
>>>>>> > For fun and learning I tried to do linear monads in a similar
>
>>>>> > On Wednesday, March 29, 2017 at 6:36:02 PM UTC-4, August Alm wrote:
>>>>> > For fun and learning I tried to do linear monads in a similar
>>>>> spirit, see: https://glot.io/snippets/eogc8rdiv1 I get the code
>>>>> > to compile (wi
gt; out; don't know what's wrong with that)
>>>> > but it does not run on glot.io, because of LIBATS/ML-dependency and
>>>> (I think) unboxed types. My take
>>>> > does not involve "name-types", just abstract proofs that an [m:
>&g
g with that)
>>> > but it does not run on glot.io, because of LIBATS/ML-dependency and
>>> (I think) unboxed types. My take
>>> > does not involve "name-types", just abstract proofs that an [m: vt0ype
>>> -> vtype] is a monad.
>>> >
I
>> think) unboxed types. My take
>> > does not involve "name-types", just abstract proofs that an [m: vt0ype
>> -> vtype] is a monad.
>> >
>> > Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>> >
>> > If we box everythin
run on glot.io, because of LIBATS/ML-dependency and (I
>> think) unboxed types. My take
>> > does not involve "name-types", just abstract proofs that an [m: vt0ype
>> -> vtype] is a monad.
>> >
>> > Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skre
then implementing functors (as is defined in
> Haskell) is straightforward
> > in ATS. However, for performance, one may not want to box everything. I
> sketched a template-based
> > implementation for functors as follows:
> >
> >
> https://github.com/githwxi/ATS-P
abstract proofs that an [m: vt0ype ->
> vtype] is a monad.
>
> Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>
> If we box everything, then implementing functors (as is defined in Haskell)
> is straightforward
> in ATS. However, for performance, one ma
onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>>
>>
>> If we box everything, then implementing functors (as is defined in
>> Haskell) is straightforward
>> in ATS. However, for performance, one may not want to box everything. I
>> sketched a template-based
ned in
> Haskell) is straightforward
> in ATS. However, for performance, one may not want to box everything. I
> sketched a template-based
> implementation for functors as follows:
>
>
> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>
nsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>>
>>
>> If we box everything, then implementing functors (as is defined in
>> Haskell) is straightforward
>> in ATS. However, for performance, one may not want to box everything. I
>> sketched a template-based
>
?
Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:
>
>
> If we box everything, then implementing functors (as is defined in
> Haskell) is straightforward
> in ATS. However, for performance, one may not want to box everything. I
> sketched a template-based
> impl
If we box everything, then implementing functors (as is defined in Haskell)
is straightforward
in ATS. However, for performance, one may not want to box everything. I
sketched a template-based
implementation for functors as follows:
https://github.com/githwxi/ATS-Postiats/blob/master/doc
41 matches
Mail list logo
