Haskell type checking and determinism

The name of the pictureThe name of the pictureThe name of the pictureClash Royale CLAN TAG#URR8PPP



Haskell type checking and determinism



According to the Haskell 2010 language report, its type checker is based on Hindley-Milner. So consider a function f of this type,


f


f :: forall a. [a] -> Int



It could be the length function for instance. According to Hindley-Milner, f type checks to Int. We can prove this by instantiating the type of f to [Int] -> Int, and the type of to [Int], then conclude that the application ([Int] -> Int) [Int] is of type Int.


f


Int


f


[Int] -> Int



[Int]


([Int] -> Int) [Int]


Int



In this proof, I chose to instantiate types forall a. [a] -> Int and forall a. [a] by substituting Int to a. I can substitute Bool instead, the proof works too. Isn't it strange in Hindley-Milner that we can apply a polymorphic type to another, without specifying which instances we use ?


forall a. [a] -> Int


forall a. [a]


Int


a


Bool



More specifically, what in Haskell prevents me from using the type a in the implementation of f ? I could imagine that f is a function that equals 18 on any [Bool], and equals the usual length function on all other types of lists. In this case, would f be 18 or 0 ? The Haskell report says "the kernel is not formally specified", so it's hard to tell.


a


f


f


18


[Bool]


f


18


0





That's a great question. Note that your function f which behaves on [Bool] differently from on other list types [a] can not exist (i.e. can not be written in Haskell) because of parametricity. In Haskell there is no way to write if a==Bool then ... and have an unaltered signature forall a. [a] -> Int.
– chi
Aug 10 at 12:07


f


[Bool]


[a]


if a==Bool then ...


forall a. [a] -> Int





See my answer below. Parametricity can be a bit overwhelming at first, but you can start from the classical "theorems for free" paper by Wadler, which shows nice examples.
– chi
Aug 10 at 12:22





I don't have a perfect reference. Parametricity is sometimes affected by bottoms (seq, infinite recursion) but I recall that assuming functions strict one can still have a weaker form of parametricity. (Again, I can't provide a reference). To completely "break" parametricity, one can use forall a. Typeable a => [a] -> Int which allows if a==Bool then ... -- but here the type changes, so it is not really broken: we have a type for parametric polymorphism and another one for ad-hoc (non-parametric) polymorphism.
– chi
Aug 10 at 21:26


seq


forall a. Typeable a => [a] -> Int


if a==Bool then ...





No, the extra a argument is not needed at all in Haskell. And even in Coq, you can't eliminate (a : Type) so there is no "if". In Coq you would need some argument to eliminate such as forall (a : Type), typeable a -> list a -> int where typeable a is suitably defined, e.g. with an inductive definition.
– chi
Aug 11 at 8:41


a


(a : Type)


forall (a : Type), typeable a -> list a -> int


typeable a





@chi Without the extra a the best I found is f l = if typeOf l == typeOf ([True]) then 18 else length l. But then f crashes with a type error. Do you see an other way ?
– V. Semeria
Aug 11 at 8:49



a


f l = if typeOf l == typeOf ([True]) then 18 else length l


f




2 Answers
2



During type inference, such type variables can indeed instantiated to any type. This may be seen as a highly non deterministic step.



GHC, for what it is worth, uses the internal Any type in such cases. For instance, compiling


Any


-# NOINLINE myLength #-
myLength :: [a] -> Int
myLength = length

test :: Int
test = myLength



results in the following Core:


-- RHS size: terms: 3, types: 4, coercions: 0
myLength [InlPrag=NOINLINE] :: forall a_aw2. [a_aw2] -> Int
[GblId, Str=DmdType]
myLength =
(@ a_aP5) -> length @ Data.Foldable.$fFoldable @ a_aP5

-- RHS size: terms: 2, types: 6, coercions: 0
test :: Int
[GblId, Str=DmdType]
test = myLength @ GHC.Prim.Any (GHC.Types. @ GHC.Prim.Any)



where GHC.Prim.Any occurs in the last line.


GHC.Prim.Any



Now, is that really not deterministic? Well, it does involve a kind of non deterministic step "in the middle" of the algorithm, but the final resulting (most general) type is Int, and deterministically so. It does not matter what type we choose for a, we always get type Int at the end.


Int


a


Int



Of course, getting the same type is not enough: we also want to get the same Int value. I conjecture that it can be proven that, given


Int


f :: forall a. T a
g :: forall a. T a -> U



then


g @ V (f @ V) :: U



is the same value whatever type V is. This should be a consequence of parametricity applied to those polymorphic types.


V



To follow-up on Chi's answer, here is the proof that f cannot depend on the type instances of f and . According to Theorems for free (the last article here),
for any types a,a' and any function g :: a -> a', then


f


f



a,a'


g :: a -> a'


f_a = f_a' . map g



where f_a is the instantiation of f on type a, for example in Haskell


f_a


f


a


f_Bool :: [Bool] -> Int
f_Bool = f



Then if you evaluate the previous equality on _a, it yields f_a _a = f_a' _a'. In the case of the original question, f_Int _Int = f_Bool _Bool.


_a


f_a _a = f_a' _a'


f_Int _Int = f_Bool _Bool



Some references for parametricity in Haskell would be useful too, because Haskell looks stronger than the polymorphic lambda calculus described in Walder's paper. In particular, this wiki page says parametricity can be broken in Haskell by using the seq function.


seq



The wiki page also says that my type-depending function exists (in other languages than Haskell), it is called ad-hoc polymorphism.





You can do ad-hoc polymorphism (and therefore write your type-dependent function) in Haskell, using a typeclass. If you do this, the type checker will force you to explicitly specify which type you're using for a.
– DarthFennec
Aug 10 at 18:58


a





@DarthFennec hum... That seems to contradict the parametricity equation above. Or the type of the function is not forall a. [a] -> Int. Can you give the exact example you're thinking of?
– V. Semeria
Aug 10 at 19:31


forall a. [a] -> Int





You're correct, sorry I wasn't clear; if you use a typeclass (let's call it Foo) to make a type-dependent function, then the type of the function must be forall a. Foo a => [a] -> Int. If we don't add the class constraint to a, then yes, parametricity dictates the function cannot be type-dependent.
– DarthFennec
Aug 10 at 19:53


Foo


forall a. Foo a => [a] -> Int


a






By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

-

Popular posts from this blog

Firebase Auth - with Email and Password - Check user already registered

Image
Clash Royale CLAN TAG #URR8PPP Firebase Auth - with Email and Password - Check user already registered I want to check when a user attempts to signup with createUserWithEmailAndPassword() in Firebase user Authentication method, this user is already registered with my app. createUserWithEmailAndPassword() 8 Answers 8 To detect whether a user with that email address already exists, you can detect when the call to createUserWithEmailAndPassword () fails with auth/email-already-in-use . I see that @Srinivasan just posted an answer for this. createUserWithEmailAndPassword () auth/email-already-in-use Alternatively, you can detect that an email address is already used by calling fetchSignInMethodsForEmail() (previous called fetchProvidersForEmail() ). fetchSignInMethodsForEmail() fetchProvidersForEmail() When the user trying to create an user with same email address, the task response will be "Response: The email address is already in use by another account." mFirebas
Read more

Dynamically update html content plain JS

Image
Clash Royale CLAN TAG #URR8PPP Dynamically update html content plain JS So I have a script bound in my index.html, which literally has to fetch an array of jsons from an api, then dynamically update my page when get response. But as a result I'm getting an as the only update of my page. here is my script fetch(url) .then((resp) => resp.json()) .then((resp) => resp.results.forEach(item => fetch(item.url) .then((response)=> response.json()) .then((response) => pokeArr.push(response)) .catch(console.log) ) ).catch(console.log) const filler = () => if(!pokeArr) return 0 pokeArr.map((i,j)=> return `<tr>$i.name</tr>` ) const pokeindex = () => document.getElementById('a').appendChild(document.createElement(filler())) pokeindex() When I'm consoling it, I can see in the console all the responses I get, so I'm at least doing the fetching part right. What's parberakan ? What's pokeArr ? – T.J. Crowder Aug 8 at 12
Read more

How to determine optimal route across keyboard

Image
Clash Royale CLAN TAG #URR8PPP How to determine optimal route across keyboard I'm trying to automate the typing process in a video game. Players are given an on-screen QWERTY keyboard layout that they can navigate with the control stick (up, down, left, right) in order to select a letter to type. I was wondering if there was a module for Python (or some other resource I could explore) that would help my program find a path across the keyboard as it types each letter in a given message. In other words, if the first letter typed was "A" and the next letter was "B", the module would know that the program should move 1 space down on the keyboard and 4 spaces to the right. Currently, I have the program resetting to the "G" key after each letter is typed (allowing me to use fixed-directions as the program parses each character in the desired message). As you can imagine, this is quite inefficient and defeats the purpose of automating the typing in the fir
Read more