[m-users.] using existential types

Philippe de Rochambeau phiroc at free.fr
Wed May 19 16:12:03 AEST 2021


I guess existential types are like typed variables in languages such as Perl 6/Raku.
For instance,

my Str $person = "Heya";

Using them is a matter of taste, to quote Zoltan.
I have yet to find a use for them.
Philippe

> Le 19 mai 2021 à 00:27, Fabrice Nicol <fabrnicol at gmail.com> a écrit :
> 
> 
> Yes, this is one aspect that comes out clearly from the manual contrastive pair reprinted below:
> 
> :- some [T] pred e_bar1(T).
> e_bar1(42).
> e_bar1(42).
> e_bar1(43).
> 	% ok (T = int)
> 
> :- some [T] pred bad_e_bar2(T).
> bad_e_bar2(42).
> bad_e_bar2("blah").
> 	% type error (cannot unify 
> types `int' and `string')
> 
> This is for procedures: you kind of lock them into one type.
> When you consider existentially quantified type constructors, understandably (yet somewhat confusingly when you are first confronted to this) the perceived semantics is the opposite: you abstract away from type instantiation into a more general kind of representation. It is quite illuminating to look at how the 'univ' type is implemented in library/univ.m. 
> More generally, type 'containers' can be concretely created this way to encapsulate items with possible alternative types, a bit like C unions. 
> 
> And yet the underlying operational logic is the same. Simply, it does not take place at the same level. 
> 
>> Le mar. 18 mai 2021 à 11:02 PM, Philippe de Rochambeau <phiroc at free.fr> a écrit :
>> Fabrice,
>> Thank you for your input.
>> I looked at the examples, but couldn’t figure out what practical use existential types might have. Perhaps a way of typing otherwise typeless parameters?
>> I guess time and practice will tell.
>> Cheers,
>> Philippe
>> 
>>>> Le 18 mai 2021 à 21:07, fabrice nicol <fabrnicol at gmail.com> a écrit :
>>>> 
>>>  Philippe,
>>> you have a set of straightforward examples pages 88-90 of the ROTD reference manual.
>>> 
>>> Also, just above:
>>> 
>>> "For procedures involving calls to existentially-typed predicates or functions, the compiler’s mode analysis must take account of the modes for type variables in all polymorphic calls. Universally quantified type variables have mode in, whereas existentially quantified type variables have mode out. "
>>> 
>>> which outlines the relationship between some [T]... and the mode system. 
>>> 
>>> (I found this relationship not entirely self-evident when I started out, but it became clearer with some practice).
>>> 
>>> Fabrice
>>> 
>>> Le 18/05/2021 à 04:00, users-request at lists.mercurylang.org a écrit :
>>>> Send users mailing list submissions to
>>>> 	users at lists.mercurylang.org
>>>> 
>>>> To subscribe or unsubscribe via the World Wide Web, visit
>>>> 	https://lists.mercurylang.org/listinfo/users
>>>> or, via email, send a message with subject or body 'help' to
>>>> 	users-request at lists.mercurylang.org
>>>> 
>>>> You can reach the person managing the list at
>>>> 	users-owner at lists.mercurylang.org
>>>> 
>>>> When replying, please edit your Subject line so it is more specific
>>>> than "Re: Contents of users digest..."
>>>> 
>>>> 
>>>> Today's Topics:
>>>> 
>>>>    1. Using existential types (Philippe de Rochambeau)
>>>>    2. Re: Using existential types (Zoltan Somogyi)
>>>>    3. Re: Transposing array2d (fabrice nicol)
>>>>    4. Re: Transposing array2d (Sean Charles (emacstheviking))
>>>> 
>>>> 
>>>> ----------------------------------------------------------------------
>>>> 
>>>> Message: 1
>>>> Date: Mon, 17 May 2021 12:12:39 +0200
>>>> From: Philippe de Rochambeau <phiroc at free.fr>
>>>> To: users at lists.mercurylang.org
>>>> Subject: [m-users.] Using existential types
>>>> Message-ID: <7f911cd8-9220-4d32-a9dd-ee177fb46190 at email.android.com>
>>>> Content-Type: text/plain; charset="utf-8"
>>>> 
>>>> An HTML attachment was scrubbed...
>>>> URL: <http://lists.mercurylang.org/archives/users/attachments/20210517/993681be/attachment-0001.html>
>>>> 
>>>> ------------------------------
>>>> 
>>>> Message: 2
>>>> Date: Mon, 17 May 2021 20:19:47 +1000 (AEST)
>>>> From: "Zoltan Somogyi" <zoltan.somogyi at runbox.com>
>>>> To: "Philippe de Rochambeau" <phiroc at free.fr>, "users"
>>>> 	<users at lists.mercurylang.org>
>>>> Subject: Re: [m-users.] Using existential types
>>>> Message-ID: <E1liaLj-0004BW-Fp at rmmprod05.runbox>
>>>> Content-Type: text/plain; charset="utf-8"
>>>> 
>>>> 
>>>> 2021-05-17 20:12 GMT+10:00 "Philippe de Rochambeau" <phiroc at free.fr>:
>>>>> Hello,could someone please explain the advantages of using existential types
>>>>> (some) in predicates as opposed to universal types?Many thanks.Best regards,
>>>> It is not question of "which is better"; they have totally different roles.
>>>> Universal types implement parametric polymorphism (the same operation
>>>> applies to all types the same way), while existential types can help implement
>>>> non-parametric polymorphism (an operation applies only to a specified set
>>>> of types, and may be implemented differently for different types).
>>>> 
>>>> People whose programming style is mostly based on functional and
>>>> logic programming tend to use parametric polymorphism almost exclusively,
>>>> because they tend to use algebraic data types instead of non-parametric
>>>> polymorphism. People whose programming style is mostly based on
>>>> object oriented programming tend to use non-parametric polymorphism,
>>>> because until recently, the popular OO languages did not support either
>>>> parametric polymorphism or algebraic data types :-(
>>>> 
>>>> Zoltan.
>>>> 
>>>> ------------------------------
>>>> 
>>>> Message: 3
>>>> Date: Mon, 17 May 2021 17:54:06 +0200
>>>> From: fabrice nicol <fabrnicol at gmail.com>
>>>> To: "Sean Charles (emacstheviking)" <objitsu at gmail.com>
>>>> Cc: users <users at lists.mercurylang.org>
>>>> Subject: Re: [m-users.] Transposing array2d
>>>> Message-ID: <2af3a9ed-1d70-8784-e49c-e8fac88b789a at gmail.com>
>>>> Content-Type: text/plain; charset="utf-8"; Format="flowed"
>>>> 
>>>> Thanks Sean, actually  the 'transpose' algorithm is encoded in file 
>>>> 'Matrix.asm', not in in Array.asm as I first thought.
>>>> 
>>>> I will look into it and see if it proves useful.
>>>> 
>>>> Fabrice
>>>> 
>>>> Le 17/05/2021 à 10:01, Sean Charles (emacstheviking) a écrit :
>>>>> On a possibly connected but probably orthogonal note, this came across 
>>>>> my radar from the SWI list, an assembly language written numerical 
>>>>> library. I don’t know if it has array transposition but somebody might 
>>>>> care to wrap it with the FFI library in the future? It does have Array 
>>>>> Functions section and moving and copying things but no explicit 
>>>>> mention on that page. The source might reveal more.
>>>>> 
>>>>> http://linasm.sourceforge.net/docs/api/array.php 
>>>>> <http://linasm.sourceforge.net/docs/api/array.php>
>>>>> 
>>>>> http://linasm.sourceforge.net/about/benchmarks.php 
>>>>> <http://linasm.sourceforge.net/about/benchmarks.php>
>>>>> 
>>>>> 
>>>>>> On 17 May 2021, at 06:50, fabrice nicol <fabrnicol at gmail.com 
>>>>>> <mailto:fabrnicol at gmail.com>> wrote:
>>>>>> 
>>>>>> I wondered whether someone ever implemented a 'transpose' procedure 
>>>>>> for array2d.
>>>>>> 
>>>>>> As there seems to be none, I have implemented a basic fallback here: 
>>>>>> https://github.com/fabnicol/RMercury/blob/library/ri.m, line 1236.
>>>>>> 
>>>>>> [Note: the library itself is very much work in progress, with 
>>>>>> numerous issues and loose ends. I'm just quoting it for reference to 
>>>>>> 'transpose'.]
>>>>>> 
>>>>>> This works, but it is the basic Cate & Twigg formula. There are 
>>>>>> numerous better options around, perhaps someone knows of some free 
>>>>>> code around?
>>>>>> 
>>>>>> Fabrice
>>>>>> 
>>>>>> 
>>>>>> _______________________________________________
>>>>>> users mailing list
>>>>>> users at lists.mercurylang.org <mailto:users at lists.mercurylang.org>
>>>>>> https://lists.mercurylang.org/listinfo/users
>>>> -------------- next part --------------
>>>> An HTML attachment was scrubbed...
>>>> URL: <http://lists.mercurylang.org/archives/users/attachments/20210517/43022076/attachment-0001.html>
>>>> 
>>>> ------------------------------
>>>> 
>>>> Message: 4
>>>> Date: Mon, 17 May 2021 16:54:39 +0100
>>>> From: "Sean Charles (emacstheviking)" <objitsu at gmail.com>
>>>> To: fabrice nicol <fabrnicol at gmail.com>
>>>> Cc: users <users at lists.mercurylang.org>
>>>> Subject: Re: [m-users.] Transposing array2d
>>>> Message-ID: <0F3EA632-2AA8-4195-98EC-CED7D91B0D9E at gmail.com>
>>>> Content-Type: text/plain; charset="utf-8"
>>>> 
>>>> As usual, it’s the naming of things that’s the hardest! I hope it proves useful…
>>>> :)
>>>> 
>>>>>> On 17 May 2021, at 16:54, fabrice nicol <fabrnicol at gmail.com> wrote:
>>>>>> 
>>>>>> Thanks Sean, actually  the 'transpose' algorithm is encoded in file 'Matrix.asm', not in in Array.asm as I first thought. 
>>>>>> 
>>>>>> I will look into it and see if it proves useful.
>>>>>> 
>>>>>> Fabrice
>>>>>> 
>>>>>> Le 17/05/2021 à 10:01, Sean Charles (emacstheviking) a écrit :
>>>>>> On a possibly connected but probably orthogonal note, this came across my radar from the SWI list, an assembly language written numerical library. I don’t know if it has array transposition but somebody might care to wrap it with the FFI library in the future? It does have Array Functions section and moving and copying things but no explicit mention on that page. The source might reveal more.
>>>>>> 
>>>>>> http://linasm.sourceforge.net/docs/api/array.php <http://linasm.sourceforge.net/docs/api/array.php>
>>>>>> 
>>>>>> http://linasm.sourceforge.net/about/benchmarks.php <http://linasm.sourceforge.net/about/benchmarks.php>
>>>>>> 
>>>>>> 
>>>>>>> On 17 May 2021, at 06:50, fabrice nicol <fabrnicol at gmail.com <mailto:fabrnicol at gmail.com>> wrote:
>>>>>>> 
>>>>>>> I wondered whether someone ever implemented a 'transpose' procedure for array2d.
>>>>>>> 
>>>>>>> As there seems to be none, I have implemented a basic fallback here: https://github.com/fabnicol/RMercury/blob/library/ri.m <https://github.com/fabnicol/RMercury/blob/library/ri.m>, line 1236. 
>>>>>>> 
>>>>>>> [Note: the library itself is very much work in progress, with numerous issues and loose ends. I'm just quoting it for reference to 'transpose'.]
>>>>>>> 
>>>>>>> This works, but it is the basic Cate & Twigg formula. There are numerous better options around, perhaps someone knows of some free code around?
>>>>>>> 
>>>>>>> Fabrice
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> _______________________________________________
>>>>>>> users mailing list
>>>>>>> users at lists.mercurylang.org <mailto:users at lists.mercurylang.org>
>>>>>>> https://lists.mercurylang.org/listinfo/users <https://lists.mercurylang.org/listinfo/users>
>>>> -------------- next part --------------
>>>> An HTML attachment was scrubbed...
>>>> URL: <http://lists.mercurylang.org/archives/users/attachments/20210517/ecfcdd58/attachment-0001.html>
>>>> 
>>>> ------------------------------
>>>> 
>>>> Subject: Digest Footer
>>>> 
>>>> _______________________________________________
>>>> users mailing list
>>>> users at lists.mercurylang.org
>>>> https://lists.mercurylang.org/listinfo/users
>>>> 
>>>> 
>>>> ------------------------------
>>>> 
>>>> End of users Digest, Vol 81, Issue 23
>>>> *************************************
>>> _______________________________________________
>>> users mailing list
>>> users at lists.mercurylang.org
>>> https://lists.mercurylang.org/listinfo/users
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/users/attachments/20210519/b9a9988b/attachment-0001.html>


More information about the users mailing list