[Haskell-cafe] Why this doesn't type checked

27 Jun 2010

      I've allways found code like
...
-- maxBound (undefined :: Int)
a bit strange as any usage of undefined is.
Being Ruby on Rails developer
I've personally found that one of the main
Rails motos is being as readable as possible.
Code must be as close to english as possible.
Embeded DSLs like rspec are made mostly to
made specs as close to english as possible.

Having this in my mind I've decided that this code should be
rewritten without undefined being mentioned. But I need some
type signature and it should mention Int type. So I've got an
idea about what I've called "fantom type functions".
So wee need type families for it to work.
...
{-# LANGUAGE TypeFamilies #-}
module Main where
import Data.Word
I want the code I've mentioned to be rewrited as something like
...
-- maxBound :: MaxBoundOf Int
As it is much more readable: "I want maxBound
with the type of MaxBound Of Int".

So here is the implementation of class Sizeable
that implements sizeof operation.
Which is type-indexed like maxBound is.
sizeof returns number of bytes that
occupy type when serialized to some
binary stream.
...
class Sizeable sizeable
  where type Sizeof sizeable
        sizeof :: Sizeof sizeable
We should like to make a default type
but GHC still doesn't support it.
...
-- type Sizeof sizeable = Int
Instances for all basic types
...
instance Sizeable Int
  where sizeof = 4
Even without defaults we get type safety in these instances
...
type Sizeof Int = Int

...
instance Sizeable Word8
  where sizeof = 1
        type Sizeof Word8 = Int
instance Sizeable Word16
  where sizeof = 2
        type Sizeof Word16 = Int
instance Sizeable Word32
  where sizeof = 4
        type Sizeof Word32 = Int
instance Sizeable Word64
  where sizeof = 8
        type Sizeof Word64 = Int
The annoyance is the need to instantiate Sizeof type family every time.
It will disappear once associated types' defaults will be implemented in GHC.

What we get with this instances is following code.
...
main =
  do print (sizeof :: Sizeof Word16)
Let's try it.

$ runhaskell this.lhs
this.lhs:78:14:
    Couldn't match expected type `Int'
           against inferred type `Sizeof sizeable'
      NB: `Sizeof' is a type function, and may not be injective
    In the first argument of `print', namely
        `(sizeof :: Sizeof Word16)'
    In the expression: print (sizeof :: Sizeof Word16)
    In the expression: do { print (sizeof :: Sizeof Word16) }

What can I do with this code to make it type-check?

-- 
Victor Nazarov