la solución de Seppo no es del todo recomendable. Siempre hay que tratar de encontrar funciones nativas de PHP en lugar de crear funciones propias. Además que el tipo doble como tal no existe según la documentación oficial que muestra los tipos de dato en php
http://mx.php.net/set_type
lee la documentación de
http://mx.php.net/number_format
esa función nativa de php soluciona tu problema, a pesar de que devuelve un String. Si por alguna razón deseas un double, puedes hacer un cast (float)
saludos