[PL-sem-jr] rest-of-summer schedule

[Artem Pelenitsyn]

Considering question of Sam on how to make return type of `IntOrString`
more specific (not just Type). I asked in Russian Telegram channel on
dependent types (yes, there are many things on Telegram), and the best
solution we came up with is like this.

import Data.List.Quantifiers

IntOrString : Bool -> (t ** Any (\x => x = t) [Int, String])
IntOrString False = (_ ** Here Refl)
IntOrString True = (_ ** There (Here Refl))

getIntOrString : (b: Bool) -> fst (IntOrString b)
getIntOrString False = 9
getIntOrString True = "Nine"

Return type of IntOrString is a type of dependent pair. It pairs a type `t`
and a proof that it is an element of type list [Int, String]. When using
the function (inside type of getIntOrString) we have to throw the proof
with `fst`.

-- Artem


чт, 18 мая 2017 г. в 14:58, Artem Pelenitsyn <artem.pelenitsyn at gmail.com>:

> Hi, guys,
>
> I created a repo for any materials for forthcoming talks. The code from my
> talk today:
>
> https://github.com/ulysses4ever/pl-sem-jr-2017-summer/blob/master/2017-05-18-idris-1/first-class-types.idr
>
> Feel free to pull-request (or mail-request the permissions for direct
> contribution).
>
> --
> Best, Artem
>
> пт, 12 мая 2017 г. в 10:16, Ayaz BADOURALY <ayaz.badouraly at student.ecp.fr
> >:
>
>>
>> Le 11/05/2017 à 18:20, Sam Caldwell a écrit :
>> >
>> > 7/13 - Ayaz on Self: The Power of Simplicity [2]
>>
>> Erf, I just realized that I'll probably be off from 7/9 to 7/15... Not
>> quite sure yet, I'll let you know as soon as possible!
>>
>> > 7/20 - Sam on Optimizing Dynamically-Typed Object-Oriented Programming
>> > Languages with Polymorphic Inline Caches [3]
>> > 7/27 - Ming-Ho on Debugging Optimized Code with Dynamic Deoptimization
>> [4]
>> > 8/3 - Ben on Optimizing Dynamically-Dispatched Calls with Run-Time
>> > Type Feedback [5]
>> > 8/10 - Nick on Customization: Optimizing Compiler Technology for Self,
>> > a Dynamically-Typed Object-Oriented Programming Language [6]
>>
>> --
>> Ayaz
>>
>>
>> _______________________________________________
>> Pl-sem-jr mailing list
>> Pl-sem-jr at lists.ccs.neu.edu
>> https://lists.ccs.neu.edu/bin/listinfo/pl-sem-jr
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed