2014-09-12

Haskell tools for satellite operations

At last week's CUFP I did a talk called “Haskell tools for satellite operations”. The abstract is:

Since 2013-04 the presenter has been supporting SSC (the Swedish Space Corporation) in operating the telecommunications satellite “Sirius 3” from its Mission Control Center in Kiruna. Functions in the satellite vendor's operations software are breaking down as the orbit of the ageing satellite degrades. To fill in the gaps in software capabilities the presenter has developed several operational tools using Haskell.
The talk will give an overview of the satellite operations environment, the tools developed in Haskell, how they benefitted (and occasionally suffered) from the choice of implementation language, which (public) libraries were critical to their success, and how they were deployed in the satellite operations environment.
A video recording of the talk is available on the CUFP page for the talk and on youtube.

If this interests you be sure to check out the other talk from the “Functional programming in space!” track; Michael Oswald's Haskell in the Misson Control Domain.

2014-02-11

Numtype(-tf) and dimensional(-tf) updated for GHC 7.8.1

My numtype and numtype-tf libraries both needed one line changes to be compatible with the GHC 7.8.1 release candidate. Versions 1.1 and 0.1.2 (respectively) have been uploaded to hackage.

The update to numtype also necessitated an update to dimensional, mainly to bump the upper bounds of the numtype dependency, but a few API additions snuck in too. The change log for the new version (0.12.3), as well as the other versions that have been uploaded to hackage since my previous version announcement can be found at the bottom of this post.

Dimensional-tf didn’t need an update for GHC 7.8 but has been updated with the same API additions as dimensional.

Dimensional’s changelog

0.13 (2014-02)

  • Bump numtype dependency to 1.1 (GHC 7.8.1 compatibility fix).
  • Added Torque.
  • Added D.. for the type synonym quantities (e.g., Angle).

0.12.2 (2013-11)

  • Added FirstMassMoment, MomentOfInertia, AngularMomentum.
  • Improved unit numerics.

0.12.1 (2013-07)

  • Typeable Dimensionals.

0.12 (2013-06)

  • Polymorphic _0 (closes issue 39).
  • Added astronomicalUnit.
  • Added imperial volume units.
  • Added ‘mil’ (=inch/1000).
  • Added tau.
  • Added KinematicViscosity.

0.10.1.2 (2011-09)

  • Bumped time dependency to < 1.5.

0.10.1.2 (2011-08)

  • Bumped time dependency to < 1.4.

0.10.1 (2011-08)

GHC 7.2.1 compatibility fix:

  • Increased CGS context-stack to 30.

2014-02-09

Joy and caution with -XNegativeLiterals in GHC 7.8

The new NegativeLiterals extension in GHC 7.8 scratches an itch I have had for a long time. Namely:

> y = (-41940.917505092) *~ kilo meter

With NegativeLiterals users of dimensional can finally write:

> y = -41940.917505092 *~ kilo meter

Thanks GHC HQ and contributors!

However, be careful so the extension doesn’t break your calculations. Here is an example (not using dimensional) of how you could get bitten. Without NegativeLiterals:

> Prelude> -2 ^ 2
> -4

With NegativeLiterals:

> Prelude> -2 ^ 2
> 4

I certainly prefer the latter behaviour, but having some regression tests in place when enabling NegativeLiterals might be a good idea.

2012-02-12

ANNOUNCE: dimensional-tf-0.10 – Statically checked physical dimensions with type families

As promised when I released numtype-tf in January I have now also created the dimensional-tf library – a conversion of the dimensional library to use Type Families instead of Functional Dependencies.

I skipped the experimental and to my knowledge unused CGS and Extensible modules. If you would like to see them ported let me know.

For straight-forward usage, e.g. the examples on the dimensional wiki, the only change required from library users to switch from dimensional to dimensional-tf is inserting .TF in the import statements. E.g.:

import Numeric.Units.Dimensional.TF.Prelude
import Numeric.Units.Dimensional.TF.NonSI

In such cases the choice of using dimensional backed by functional dependencies or type families is largely philosophical as neither will be visible in the client code.

If you do more advanced things with polymorphic dimensions and explicit type signatures you will have to convert the type signatures from MLTC style constraints to type families. E.g.:

myFunc :: (Num a, Mul d1 d2 d3) => Quantity d1 a -> Quantity d2 a -> Quantity d3 a

would change to:

myFunc :: Num a => Quantity d1 a -> Quantity d2 a -> Quantity (Mul d1 d2) a

Compiler errors will also be different in dimensional-tf, for better or for worse.

So, should you use dimensional or dimensional-tf? For the time being I consider dimensional-tf to be experimental. If you want stability stick with dimensional for now. If your dislike of functional dependencies trumps your need for stability, then try dimensional-tf. If dimensional-tf eventually proves itself to be a better dimensional I will merge it into the latter with a major version bump.

Dimensional-tf-0.1 compiles on GHC-7.0. The source code is on Github.

Update 2012-02-15: In case this wasn't building for you on GHC-7.4.1; I've added a FlexibleInstances pragma that should take care of it. Dimensional-tf-0.1.0.1 compiles on GHC-7.0 and 7.4.

Flattr this

2012-01-25

Type level integers with Type Families (numtype-tf 0.1)

Pretty much since they were introduced into GHC I’ve been meaning to try to port the dimensional library to use Type Families instead of Functional Dependencies. However, functional dependencies have served me quite well and I’ve been lacking the inspiration to dig into type families. That is, until I read the Leonidas’ Statically Typed Vector Algebra Using Type Families. Leonidas’ blog post resonated with me as the problem it addresses is related to one I myself have been interested in for some time (linear algebra with static guarantees). It also gave me a clear vision of how to apply type families to the fundamendal problem of dimensional – type level integers.

I’ve implemented the numtype-tf library which is in essence numtype using type families (hence the “-tf”) instead of functional dependencies. Some of my design decisions are slightly different (beside the choice of type system extension), e.g. the representation of negative integers is different and the PosType and NegType classes have been dropped in numtype-tf. The haddocks have also been improved a little.

A feature of the functionally dependent numtype that I was unable to reproduce with type families is ”mutual dependencies”, used in the Sum and Div type classes of numtype. Here is an example of type signatures (instances omitted) and ghci usage:

> class Sum a b c | a b -> c, a c -> b, b c -> a
> (+) :: (Sum a b c) => a -> b -> c
> (-) :: (Sum a b c) => c -> b -> a
\*Numeric.NumType> pos3 - pos5
NumType -2

To the best of my knowledge corresponding code with type families would be along the lines of:

> type family Sum a b
> (+) :: a -> b -> Sum a b
> (-) :: Sum a b -> b -> a
\*Numeric.NumType.TF> pos3 - pos5

<interactive>:1:1:
    Couldn't match type `Sum a0 Pos5' with `S Pos2'
    …

In order for the latter to compute we must assist the type checker by being explicit about the type of a0, i.e. pos3 - pos5 :: Neg2, which largely defeats the purpose of type level arithmetic. Instead two type families are used in numtype-tf:

> type family Add a b  -- a + b
> (+) :: a -> b -> Add a b
> type family Sub a b -- a - b.
> (-) :: a -> b -> Sub a b

This works OK but the lack och mutual dependencies in type families restricts what I will losely refer to as “type inference back tracking”. This may or may not be a significant drawback compared to fundep numtype depending on the use case.

If you are interested in comparing code written with type families to code written with functional dependencies take a look at the respective modules on Github: Numeric.NumType.TF vs. Numeric.NumType.

The next step is to reimplement dimensional as dimensional-tf in order to exercise numtype-tf and better understand the impact of the differences with respect to numtype. I am also looking forward to playing with GHC.TypeNats in GHC 7.4.

Flattr this

2011-09-15

Yesod Cookbook: Internationalized Form

I posted the following example of an internationalized form to the Yesod Cookbook a few days ago. Yesod has a pretty awesome library for programming with forms and also a flexible but currently under-documented system for internationalization. However, how the two interact, while straightforward, might not be immediately obvious to the newcomer. Hence the motivation for the below example which shows how to internationalize both custom messages and Yesod's built-in FormMessages (mostly form error messages).

Familiarity with Yesod at the level of the Yesod Book is assumed.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
{-

INTERNATIONALIZED FORM

Below is an example of how to internationalize a Yesod application,
including internationalization (i18n) of a form and Yesod's built-in
form error messages.

In the example we create a simple site that will show messages in
Swedish or English depending on the browser's preferred language.
If neither Swedish or English are preferred languages the site will
default to Swedish.

Familiarity with Yesod at the level of the Yesod book is assumed,
comments are concentrated to the parts relevant to i18n.

-}

{-# LANGUAGE QuasiQuotes
           , TemplateHaskell
           , MultiParamTypeClasses
           , OverloadedStrings
           , TypeFamilies
  #-}

import Yesod
import Yesod.Form.I18n.Swedish
import Control.Applicative ((<$>), (<*>))
import Data.Text (Text)


-- Our foundation data type.
data MyApp = MyApp

mkYesod "MyApp" [parseRoutes|
/    RootR GET
|]

instance Yesod MyApp where
    approot _ = ""


-- Here we provide internationalization of Yesod's built in form
-- messages (mostly error messages). For brevity it is assumed that
-- Swedish translations are exported as 'swedishFormMessage' by the
-- module Yesod.Form.I18n.Swedish (an implementation can be copied
-- from https://gist.github.com/1209328).
instance RenderMessage MyApp FormMessage where
    renderMessage _ []        = swedishFormMessage -- Default to Swedish
    renderMessage _ ("sv":ls) = swedishFormMessage
    renderMessage _ ("en":ls) = defaultFormMessage -- English
    renderMessage m (_   :ls) = renderMessage m ls

-- Next we define the custom messages present on the site and their
-- rendering functions for different languages.
data Msg = Model
         | Year
         | Please

-- Rendering function for English.
renderEnglish Model  = "Model"
renderEnglish Year   = "Year"
renderEnglish Please = "Please fill in your car's details"

-- Rendering function for Swedish.
renderSwedish Model  = "Modell"
renderSwedish Year   = "Årgång"
renderSwedish Please = "Vänligen fyll i uppgifterna för din bil"

-- The instance used to select the appropriate rendering function.
-- This is almost identical to the instance for FormMessage above.
instance RenderMessage MyApp Msg where
    renderMessage _ []        = renderSwedish -- Default to Swedish
    renderMessage _ ("sv":ls) = renderSwedish
    renderMessage _ ("en":ls) = renderEnglish
    renderMessage m (_   :ls) = renderMessage m ls


-- The data model.
data Car = Car
    { carModel :: Text
    , carYear :: Int
    }
  deriving Show

-- In our form we use our messages Model and Year as field labels.
carAForm :: AForm MyApp MyApp Car
carAForm = Car
    <$> areq textField (fs Model) Nothing
    <*> areq intField  (fs Year)  Nothing
    where
        fs msg = FieldSettings msg Nothing Nothing Nothing

carForm :: Html -> Form MyApp MyApp (FormResult Car, Widget)
carForm = renderTable carAForm


-- Our handler just shows the form, with submitted values pre-filled.
-- Here we also use the Please message.
getRootR :: Handler RepHtml
getRootR = do
    ((_, widget), enctype) <- runFormGet carForm
    defaultLayout [whamlet|
        <p>_{Please}
        <form method=get action=@{RootR} enctype=#{enctype}>
            <table
                ^{widget}
            <p><input type=submit>
        |]


-- | Launch the app on port 3000.
main :: IO ()
main = warpDebug 3000 MyApp

Flattr this

2011-06-17

Toy URL shortener with Yesod and acid-state

Updated 2011-08-31: Modified urlForm to work with Yesod 0.9.1.

Herein we will create a rudimentary unsafe URL shortener – a toy. We will see how to use David Himmelstrup’s acid-state to persist a data structure and how to use Michael Snoyman’s Yesod to build a simple web application.

This URL shortener is unsafe not in the sense of unsafePerformIO or unsafeCoerce, but in the sense that it is wide open to abuse. If you use it as anything other than a toy The Internet (spammers et al) will have you for breakfast. Jason Jacek has written a good article on the good and bad of URL shorteners; if you are looking for a non-toy URL shortener use one of the products he recommends.

This post is literate Haskell; just copy and paste it into a .lhs file and build/run with GHC.

Preliminaries

Language extensions, imports, and all that. There’s just no way around them!

> {-# LANGUAGE DeriveDataTypeable #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE OverloadedStrings #-}
> {-# LANGUAGE QuasiQuotes #-}
> {-# LANGUAGE StandaloneDeriving #-}
> {-# LANGUAGE TemplateHaskell #-}
> {-# LANGUAGE TypeFamilies #-}
> import Control.Exception (bracket)
> import Control.Monad.Reader (asks)
> import Control.Monad.State (gets, put)
> import Data.Acid
> import Data.IntMap (IntMap, Key, empty, insert, lookup)
> import Data.SafeCopy
> import Data.Text (Text)
> import Data.Typeable
> import Prelude hiding (lookup)
> import System (getArgs)
> import Yesod hiding (Key, insert, Update, update, get)
> type URL = Text
> -- type Key = Int is provided by Data.IntMap.

State

We first create an appropriate (for some definition of appropriate) data structure for storing URLs. Then we will give that data structure ACID (Atomicity, Consistency, Isolation and Durability) guarantees by way of the acid-state package.

URL storage data structure

We’re going to keep things real simple and stuff our URLs into an IntMap using sequentially increasing keys. We also keep track of the latest key assigned.

> data URLStore = URLStore Key (IntMap URL)

Now we create the API we will use for our URL store. We need to be able to create an empty store, add URLs, and retrieve the URL corresponding to a given key.

> -- | Create an empty store.
> emptyStore :: URLStore
> emptyStore = URLStore 0 empty
> -- | Add an URL to the store. Return the key to the URL together
> -- with the updated store.
> addURL :: URL -> URLStore -> (Key, URLStore)
> addURL u (URLStore n m) = let k = n+1 in (k, URLStore k (insert k u m))
> -- | Retrieve an URL from the store.
> retrieveURL :: Key -> URLStore -> Maybe URL
> retrieveURL k (URLStore _ m) = lookup k m

Nothing fancy going on so far, just the plain everyday Haskell you know and love!

Make our URL store ACIDic with acid-state

Now we’ll take our vanilla URL store and make it ACIDic using acid-state. First we’ll need Typeable and SafeCopy instances.

> deriving instance Typeable URLStore
> $(deriveSafeCopy 0 'base ''URLStore)

We also have to “port” the add/retrieve API to be ACIDic.

> -- | Add an URL to the ACIDic store. Return the key to the URL.
> add :: URL -> Update URLStore Key
> add u = do
>   (k, store) <- gets (addURL u)
>   put store
>   return k
> -- | Retrieve an URL from the ACIDic store.
> retrieve :: Key -> Query URLStore (Maybe URL)
> retrieve = asks . retrieveURL

Finally, let some magic happen and, ta-da, we have our ACIDic URL store! In particular this creates Add and Retrieve data constructors that will be used below as proxies for add and retrieve.

> $(makeAcidic ''URLStore ['add, 'retrieve])

The Yesod web app

All that is missing now is the web app that will use our ACIDic state. We’ll use Yesod to for that but only scratch the surface of all the good stuff Yesod can do (including persistence).

Seth Falcon has written a survey of URL shortening service APIs. Our API will is very basic: POST a href parameter to / to get a short URL (a GET will also do the job, I’ll let convenience trump idempotency here).

First we define the Yesod foundation type URLShort and make it an instance of Yesod. The foundation will have to carry its state.

> data URLShort = URLShort { state :: AcidState URLStore }
> instance Yesod URLShort where approot _ = ""

Then we define routes (paths) we will use. #Key will match any leading integer and discard trailing junk.

> mkYesod "URLShort" [parseRoutes|
> /      RootR      GET POST
> /#Key  RedirectR  GET
> |]

URL Shortening

The route handlers for / do the URL shortening. The only difference between a GET and a POST is where the query params come from.

> getRootR  = lookupGetParams  "href" >>= doRootR
> postRootR = lookupPostParams "href" >>= doRootR

When given a single URL store it and display its key and a HTML form for submitting another URL.

> doRootR [url] = do
>   acid <- fmap state getYesod
>   key  <- update' acid (Add url)
>   defaultLayout $ do
>     addHamlet [hamlet|<a href=@{RootR}#{key}>@{RootR}#{key}|]
>     addWidget urlForm  -- Is this "The Right Way"?

Otherwise display only the form.

> doRootR _ = defaultLayout urlForm

Here is the HTML form (we don’t bother with fancy formlets).

> urlForm = [whamlet|
> <form action=@{RootR} method=post
>   <input type=text name=href
>   <input type=submit value=Shorten!
> |]

Redirecting

The route handler for /[0–9]* retrieves the appropriate URL and redirects the client. If no URL is found for the key the client is given a 404.

> getRedirectR key = do
>   acid <- fmap state getYesod
>   url  <- query' acid (Retrieve key)
>   case url of
>     Just u  -> redirectText RedirectPermanent u
>     Nothing -> notFound
>   return ()

The return () at the end is there to help GHC infer a suitable type of getRedirectR.

Applicationification (main)

Our main runs the yesod application with its AcidState. The port number to run on must be provided. Bad arguments crash (I already mentioned that this is a toy, right?). A bracket ensures that the AcidState is checkpointed and closed on exit.

> -- Provide port number as argument.
> main = do
>   port <- fmap (read . head) getArgs
>   bracket (openAcidState emptyStore)
>           createCheckpointAndClose
>           (warpDebug port . URLShort)

Thanks to the magic of acid-state our URL store is persistent across executions. Go ahead, try it out!

Exercises

You can move this URL shortener a teenie bit further from toydom and closer to tooldom by implementing one or more of the following:

  • Use denser representation than decimal digits;
  • Don’t store duplicate URLs (reuse old key);
  • URL preview;
  • JSON, XML, and raw text content;
  • Sanity-check submitted URLs;
  • Filter spam URLs;

From there move on to authentication, statistics, and so on…

Thanks for reading!

Flattr this