Fair point - and it does make sense. Since it is a completely unbound type var a I can never assign it a value in Elm, so setting it to Never should always type check since it will never be able to contradict any value in the program.
The one exception would be if the free type var is number, because you can create numbers in Elm. But a free number can always be replaced by Int or Float to derive an equivalent program with zero unbound type vars.
yes. There are also appendable and comparable and I think thatās all? All of these are special variable prefixes that also carry an explicit constrain. But by design are impossible to combine in elm. You canāt have appendable number. And all number are comparable otherwise you couldnāt use Set Int. Number is special because you can construct value that is number. You canāt construct value that is comparable. What you can construct is some concrete type of comparable but not a value of type comparable.
One thing to realize about these constrained type variables is that they donāt exist in type definition itself. Only in function implementation. This is legal:
type alias NoConstraintDict a b = Dict a b
but you wonāt be able to put any a in dict because functions to insert is where constraint applies. In reality these works like:
type Dict a b
insert : Comparable a => a -> b -> Dict a b -> Dict a b
the constrain is property of the function insert, not the dict type.
So here is an interesting program for you. It has Model number and it even does increment the number without knowing what type it is. What it canāt do is to display number. Because to convert it to String there is no function number -> String only Float -> String and Int -> String.
module Main exposing (main)
import Browser
import Html exposing (Html, button, div, text)
import Html.Events exposing (onClick)
import Dict exposing (Dict)
type alias NoConstraintDict a b = Dict a b
type alias Model a =
{ count : a }
initialModel : Model number
initialModel =
{ count = 0 }
type Msg
= Increment
| Decrement
update : Msg -> Model number -> Model number
update msg model =
case msg of
Increment ->
{ model | count = model.count + 1 }
Decrement ->
{ model | count = model.count - 1 }
view : Model number -> Html Msg
view model =
div []
[ button [ onClick Increment ] [ text "+1" ]
, button [ onClick Decrement ] [ text "-1" ]
]
main : Program () (Model number) Msg
main =
Browser.sandbox
{ init = initialModel
, view = view
, update = update
}
Hopefully that gives you full idea about why I and some others keep bringing this discussion back from type variables to these constrained type variables. Especially the number because that one has literal which is constrained type variable you can construct (like 0, 0 + 1).
EDIT: Just realized we can stay in development build and use Debug.toString. So here you have Counter example in elm which is actually working with number, incrementing it and decrementing it while not knowing if itās Int or Float.
module Main exposing (main)
import Browser
import Dict exposing (Dict)
import Html exposing (Html, button, div, text)
import Html.Events exposing (onClick)
type alias Model a =
{ count : a }
initialModel : Model number
initialModel =
{ count = 0 }
type Msg
= Increment
| Decrement
update : Msg -> Model number -> Model number
update msg model =
case msg of
Increment ->
{ model | count = model.count + 1 }
Decrement ->
{ model | count = model.count - 1 }
view : Model number -> Html Msg
view model =
div []
[ button [ onClick Increment ] [ text "+1" ]
, div [] [ text <| Debug.toString model.count ]
, button [ onClick Decrement ] [ text "-1" ]
]
main : Program () (Model number) Msg
main =
Browser.sandbox
{ init = initialModel
, view = view
, update = update
}
I think this is closest we get to āweird untyped programā. ellie
Many languages require floats to have a decimal in them, so:
1 : Int
1.0 : Float
Elm is a bit unusual in allowing 1 : number. It is convenient:
x = 1 + 2.0 -- Fine its Float
But I also wonder if knowing that both would compile to Javascript number influenced that language choice, since it does not really matter in that situation.
I find the conversation and concern fascinating having spent time in PureScript and Haskell using a tagless final style. I was always working with deep abstractions (higher kinded type variables), none of my code knew which concrete thing it would use, AND YET I always felt perfectly calm and safe in the knowledge that my program was sound in its own context thanks to the HM type system.
I get the question about the top level program. That is an interesting situation where our programs get run by an engine (the Elm architecture) and we have to trust that engine to do right by the programs we declare.
However, INSIDE the functionsā¦ trust the type system. For me that is the joy of functional programming. It is so calming because we can trust.
@rupert, if you havenāt toyed with PureScript/Haskell tagless final syntax Iāll give an example
guessingGame :: forall m. Console m => RandomInt m => m Unit
guessingGame = do
writeStrLn "Enter a number (1 to 100) or 'quit'"
numberStr <- readStrLn
when (numberStr /= "quit") do
myNumber <- randomInt { start: 1, end: 100 }
writeStrLn $
case (Data.Int.fromString numberStr) of
Nothing -> "Not a number. Try again."
Just myNumber -> "You win!"
Just _ -> "You lose... sorry"
guessingGame -- recurse.
In the code above the two constraints on m (the game monad) say that it requires the two capabilities 1. the ability to read and write an abstract Console and 2. the ability to generate random numbers.
The capabilities are type classes. They are abstract and would be defined in a separate module. They act a bit like interfaces in OO and can be used to represent Ports in a hexagonal architecture (Ports and Adapters). So they might look like this
class Console m where
readStrLn :: m String
writeStrLn :: String -> Unit
class RandomInt m where
randomInt :: { start :: Int, end :: Int } -> m Int
The guessing game is completely abstract over the actual monad in which it runs. You write a lot of code like that in PureScript/Haskell so pretty much all code has to trust that types unify and that everything will be OK even if you have types of types of types of types (given the higher kindedness).
When you actually want to run the guessing game it has to be in a concrete monad. The fun thing is that for the real application monad it can be effectful and for the unit tests it would probably be pure. That means that your real application has effects and talks to the outside world while your unit tests would probably furnish the guessing game with mock readStrLn input and random numbers from a specified buffer and then would capture the output in an array. You might then end up writing your tests like
it "when quitting immediately" do
runGuessingGameWithInput { readStrLns: [ "quit" ], randomNumbers: [] }
`shouldEqual` { outputLines: [], unreadLines: [] }
it "when entering a bad number and then quitting" do
runGuessingGameWithInput
{ readStrLns: [ "blah", "quit" ], randomNumbers: [] }
`shouldEqual`
{ outputLines: [ "Not a number. Try again."
, unreadLines: []
}
it "when entering a good guess" do
runGuessingGameWithInput
{ readStrLns: [ "10", "quit" ], randomNumbers: [10] }
`shouldEqual`
{ outputLines: [ "You win!"
, unreadLines: []
}
-- etc. etc..
But I also wonder if knowing that both would compile to Javascript number influenced that language choice, since it does not really matter in that situation.
I think only Evan can answer that. But my two cents are that this was inspired by Haskell where this also works like this. OCaml for instance requires . in floats and doesnāt even have adhoc polymorphism on operators. + is addition on ints, +. is addition on floats. I would guess Evan who doesnāt like syntax noise aesthetically and also wants thing to be intuitive likes Haskell way more even though there is more going on in the language to make it happen. But the way itās implement has a lot to do with JS I think. But itās also a bit of a curse like for that ^ bug.
Tangles final seems to be quite popular. We also use it at work (Haskell). But to be honest I donāt see people really utilizing decoupling as much as they would like to make you believe they do. Like at work we really have just 2 implementations of the monad that runs whole application - one for tests and one for everything else. And even then itās sometimes hard to explain to people that they can actually utilize it as itās meant to be. Considering this parametrization creates all sorts of optimization barriers for the compiler Iām not even sure if itās worth it. For sure there are some cases where one can gain a great millage from this sort of decoupling Iām just not sure if theyāre that common. What I know for sure is that to really keep the benefits of this one has to be very disciplined about decoupling the interface from implementation details. Like in our case there are Amazonka (haskell library for amazon apis) specific types used as arguments in these class methods/functions which I would argue break the logical decoupling. And even people who advocate for it often break principles that make it useful to begin with. But maybe itās just me being a bit over āall the things type we can do with type systemsā. These days Iām frankly more concerned with compile times than with type system features.
When I first saw tagless final I got goosebumps because it seemed like such an elegant way to solve the āeffect problemā and Iāve never need to introspect on my programs in a business application context so Free Monads didnāt seem worth it.
However, your experience also aligns with mine: thereās pretty much only ever two instances (application and test), it does make things more difficult for the compiler, contributes to worse error messages for engineers, and your point about implementation leaks is so hilariously true. Like if you have a type class for abstracting a concrete Api that has tons of sum types and you have to re-implement a significant subset of those sum types and then map them in order to decouple. It can start to feel performative: āLook at me ma! Iām being abstract.ā.
This article The False Hope of Managing Effects with Tagless-Final in Scala ā John A De Goes says a lot of relevant things on the subject. Some of the points apply only to Scala but most apply.
This resonates with me very strongly. I am in the same place. A slow compiler with terrible error messages removes agency from the software engineer. Iāve also used āfancyā type class engineering to generate code and thought I was cleverā¦ but then no one could understand what I had done because it wasnāt strictly the lambda calculus (with pattern matching it kinda looks closer to Prolog) and no one could debug the code AND the application compile times went straight into the toilet. I think that elm-review-derive is actually far superior - and I know a lot of my FP colleagues would view that as heresy. 
In mentioning tagless final I was just trying to observe that in a lot of PureScript/Haskell code there is often one to several highly constrained type variables pretty close to the top of the application, and that creates a need to trust the abstractions and the type system. In this conversation I sensed a little anxiety around whether type variables at the top was āOkayā, and I suppose I am saying that it is.
Clearly we have a lot of similar experience and thoughts here. I donāt remember I ever had a feeling that someone understood what Iām trying to say that well. And I know it canāt be because I expressed myself so clearly because I know I did not. So the only logical explenation is that we had similar point of view before the interaction already. Thanks for the blogpost I was not aware of it. Iām putting to read leter but even from the title alone Iām pretty sure I will enjoy it.