Re: [Haskell-cafe] Re: practicality of typeful programming

28 Jun 2007

      Hi Daniil,

I had a look at the paper and associated code that Oleg refers to there is no 
special parsing taking place:

From Vector/read-examples.hs:

v3 = do
    let m1 = $(dAM [[1,2],[3,4]])
    s <- readFile "Vector/example-data.txt"
    listMatRow (read s) (\(m2::AVector Double a) ->
        print $ m2 *> trans m1
      )

It does not make any difference if the list that is used to populate the 
matrix is specified in the code or read from a file. 

In both cases, if the list lenght is incorrect, an error is generated at 
run-time (I think, I cannot run the actual code).

The TH trickery, that Oleg refers to, is there to solve a different problem:

<quote>
Note that in each example we print the matrix _inside_ the function
argument to the list* functions. We cannot, for instance, just return
it, because this causes a universally quantified type to escape:
...
listVec_ [1,2,3] (\v -> v)
<interactive>:1:0:
    Inferred type is less polymorphic than expected
      Quantified type variable `n' escapes
    In the second argument of `listVec', namely `(\ v -> v)'
    In the definition of `it': it = listVec [1, 2, 3] (\ v -> v)
This is why it is not possible to have a function which takes a list
and returns a vector of unknown type. The 'fromList' member of the
Vector class is only used when we want to turn a list into a vector
whose type is known in advance. (see v4 below)
</quote>

So, in order to play around with matrices of unknown type in GHCi what they do 
(if I read the code correctly) is to convert the matrix to TH, specifying the 
exact type, and compiling/splicing it back:

liftVec :: (GetType e, Lift e, GetType a, Dom a, Vector v e, GetType (v a))
    => v a -> ExpQ
liftVec (v::v a) = do
  es <- lift (elems v)
  let at = getType (__::a)
  let et = getType (eltType v)
  let vt = getType (__::(v a))
  return $
    (SigE
      (AppE (VarE $ mkName "fromList")
          (SigE es (AppT ListT et)))
      vt
    )

Crazy haskellers.

Is it just me that some time thinks with nostalgia to Apple II Basic?

Best,

       titto

On Thursday 28 June 2007 15:38:17 Daniil Elovkov wrote:
...
2007/6/28, Pasqualino 'Titto' Assini :
...
On Wednesday 27 June 2007 23:28:44 oleg@pobox.com wrote:
...
In his system, the type of the matrix includes includes the matrix
size and dimensions, so invalid operations like improper matrix
multiplication can be rejected statically. And yet, his library
permits matrices read from files.
Read from files but still at compile time, correct?
(titto, sorry for dupliate)
No, what is meant, I believe, is reading from a file at run-time and
parsing this way
(u :: UnTyped) <- readFromFile
case parse u of
    Nothing -> -- failed to parse, because those data wouldn't
satisfy constraints
    Just (t::Typed) ->
       -- if we're here, we have the typed t, and there are garantees
that it is well formed
       -- in terms of our invariants
parse :: UnTyped -> Maybe Typed
so deciding whether we have correct data is made at run-time, by
calling parse and examining its return value.