Proposal: Fixed length lists and restricted number types

[dta]

I think you’ll find @Lucas_Payr’s maser thesis work very interesting:

Elm-Refine: Proposal

Greetings everyone, I’m currently studying computer mathematics at the University of Linz/Austria and am now working on my master-thesis: Refinement types for Elm. In this post I will first explain the main concept and then propose a syntax. I would be grateful if you could give me feedback regarding the syntax. What are Refinement Types? Let’s look at the following example. {-| @refine \int -> int /= 0 -} type alias IntWithoutZero = Int dividedBy : IntWithoutZero -> Int -> Int dividedBy…

second-presentation.pdf