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.