Data.Proxy

Short note on Data.Proxy based on this Stackoverflow answer.

First, a few imports:

> {-# LANGUAGE RankNTypes          #-}
> {-# LANGUAGE ScopedTypeVariables #-}
>
> module Proxy where
>
> import Data.Proxy
> import Text.Read

Suppose we want to check if some fuzzy real world data can be read as certain concrete types. We could write a few helper functions using readMaybe:

> readableAsInt :: String -> Bool
> readableAsInt s
>   = case readMaybe s of
>       Just (_ :: Int) -> True
>       _               -> False
>
> readableAsDouble :: String -> Bool
> readableAsDouble s
>   = case readMaybe s of
>       Just (_ :: Double) -> True
>       _                  -> False
>
> readableAsBool :: String -> Bool
> readableAsBool s
>   = case readMaybe s of
>       Just (_ :: Bool) -> True
>       _                -> False

These are all basically the same. How to generalise? Let’s try a typeclass.

> class ReadableAs t where
>    readableAs :: String -> Bool

This doesn’t work since readableAs doesn’t depend on the type t:

    The class method ‘readableAs’
    mentions none of the type or kind variables of the class ‘ReadableAs t’
    When checking the class method: readableAs :: String -> Bool
    In the class declaration for ‘ReadableAs’
Failed, modules loaded: none.

So put the type in:

> class ReadableAs' t where
>    readableAs' :: t -> String -> Bool

This compiles, so let’s write some instances:

> instance ReadableAs' Int where
>   readableAs' _ s
>      = case readMaybe s of
>          Just (_ :: Int) -> True
>          _               -> False
>
> instance ReadableAs' Double where
>   readableAs' _ s
>      = case readMaybe s of
>          Just (_ :: Double) -> True
>          _                  -> False
>
> instance ReadableAs' Bool where
>   readableAs' _ s
>      = case readMaybe s of
>          Just (_ :: Bool) -> True
>          _                -> False

Using it is clunky since we have to come up with a concrete value for the first argument:

 > readableAs' (0::Int) "0"
 True
 > readableAs' (0::Double) "0"
 True

For some types we could use Data.Default for this placeholder value. But for other types nothing will make sense. How do we choose a default value for Foo?

> data Foo = Cat | Dog

Haskell has non-strict evaluation so we can use undefined, but, ugh. Bad idea.

 > readableAs' (undefined::Int) "0"
 True

So let’s try out Proxy. It has a single constructor and a free type variable that we can set:

 > :t Proxy
 Proxy :: Proxy t
 > Proxy :: Proxy Bool
 Proxy
 > Proxy :: Proxy Int
 Proxy
 > Proxy :: Proxy Double
 Proxy

Let’s use Proxy t instead of t:

> class ReadableAsP t where
>    readableAsP :: Proxy t -> String -> Bool
>
> instance ReadableAsP Int where
>   readableAsP _ s
>      = case readMaybe s of
>          Just (_ :: Int) -> True
>          _               -> False
>
> instance ReadableAsP Double where
>   readableAsP _ s
>      = case readMaybe s of
>          Just (_ :: Double) -> True
>          _                  -> False
>
> instance ReadableAsP Bool where
>   readableAsP _ s
>      = case readMaybe s of
>          Just (_ :: Bool) -> True
>          _                -> False

This works, and we don’t have to come up with the unused concrete value:

 > readableAsP (Proxy :: Proxy Bool) "0"
 False
 > readableAsP (Proxy :: Proxy Bool) "True"
 True
 > readableAsP (Proxy :: Proxy Int) "0"
 True
 > readableAsP (Proxy :: Proxy Double) "0"
 True
 > readableAsP (Proxy :: Proxy Double) "0.0"
 True

Still, there’s a lot of duplication in the class and instances. We can do away with the class entirely. With the ScopedTypeVariables language extension and the forall, the t in the type signature can be referred to in the body:

> readableAs :: forall t. Read t => Proxy t -> String -> Bool
> readableAs _ s
>      = case readMaybe s of
>          Just (_ :: t) -> True
>          _             -> False
 > readableAs (Proxy :: Proxy Int) "0"
 True
 > readableAs (Proxy :: Proxy Int) "foo"
 False

Archived comments


Franklin Chen

2017-03-25 02:23:07.94742 UTC

This can also now be done without Proxy, thanks to explicit type application:

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Maybe (isJust)

readableAs :: forall t. Read t => String -> Bool
readableAs = isJust @t . readMaybe

example1 = readableAs @Int "0"
example2 = readableAs @Int "foo"
example3 = readableAs @Double "0.1"

ghc-imported-from => ghc-mod (March 2017)

I have a pull request to merge ghc-imported-from into ghc-mod. The main benefit of being part of ghc-mod is that I don’t have to duplicate ghc-mod’s infrastructure for handling sandboxes, GHC options, interfaces to other build tools like Stack, and compatibility with more versions of GHC.

The pull request is still under review, so until then you can try it out by cloning the development branches:

git clone -b imported-from https://github.com/DanielG/ghc-mod.git ghc-mod-imported-from
cd ghc-mod-imported-from
cabal update && cabal sandbox init && cabal install
export PATH=`pwd`/.cabal-sandbox/bin:$PATH

Assuming that you use Plugged for managing Vim/Neovim plugins, use my branch of ghcmod-vim by adding this to your vimrc:

call plug#begin('~/.vim/plugged')

Plug 'carlohamalainen/ghcmod-vim', { 'branch': 'ghcmod-imported-from-cmd', 'for' : 'haskell' }

Install the plugin with :PlugInstall in vim.

Here are some handy key mappings:

au FileType  haskell nnoremap            :GhcModType
au FileType  haskell nnoremap            :GhcModInfo
au FileType  haskell nnoremap    :GhcModTypeClear

au FileType lhaskell nnoremap            :GhcModType
au FileType lhaskell nnoremap            :GhcModInfo
au FileType lhaskell nnoremap    :GhcModTypeClear

au FileType haskell  nnoremap   :GhcModOpenDoc
au FileType lhaskell nnoremap   :GhcModOpenDoc

au FileType haskell  nnoremap   :GhcModDocUrl
au FileType lhaskell nnoremap   :GhcModDocUrl

au FileType haskell  vnoremap  : GhcModOpenHaddockVismode
au FileType lhaskell vnoremap  : GhcModOpenHaddockVismode

au FileType haskell  vnoremap  : GhcModEchoUrlVismode
au FileType lhaskell vnoremap  : GhcModEchoUrlVismode

On the command line, use the imported-from command. It tells you the defining module, the exporting module, and the Haddock URL:

$ ghc-mod imported-from Foo.hs 9 34 show
base-4.8.2.0:GHC.Show.show Prelude https://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html

From Vim/Neovim, navigate to a symbol and hit F4 which will open the Haddock URL in your browser, or F5 to echo the command-line output.

Raspbian with full disk encryption

This blog post shows how to convert a standard Raspbian installation to full disk encryption. The encryption passphrase can be entered at the physical console or via a dropbear ssh session.

I mainly follow the Offensive Security guide.

What you need:

  • Raspberry Pi.
  • Laptop with a microSD card slot. I used my X1 Carbon running Ubuntu xenial (amd64).

First, install Raspbian. With a 32Gb microSD card the partitions are:

/dev/mmcblk0p2                29G  4.8G   23G  18% /media/carlo/7f593562-9f68-4bb9-a7c9-2b70ad620873
/dev/mmcblk0p1                63M   21M   42M  34% /media/carlo/boot

It’s a good idea to make a backup of the working installation:

dd if=/dev/mmcblk0 of=pi-debian-unencrypted-backup.img

Also make a note of the start/end of the main partition. This will be needed later.

Install the qemu static (on the laptop, not the Pi):

sudo apt update
sudo apt install qemu-user-static

Create directories for the chroot. Easiest to do all of this as root. Pop the sd card into the laptop and drop into a chroot:

mkdir -p pi/chroot/boot

mount /dev/mmcblk0p2 pi/chroot/
mount /dev/mmcblk0p1 pi/chroot/boot/

mount -t proc  none     pi/chroot/proc
mount -t sysfs none     pi/chroot/sys
mount -o bind /dev      pi/chroot/dev
mount -o bind /dev/pts  pi/chroot/dev/pts

cp /usr/bin/qemu-arm-static pi/chroot/usr/bin/
LANG=C chroot pi/chroot/

Next we need to install a few things in the chroot. If these fail with

root@x4:/# apt update
qemu: uncaught target signal 4 (Illegal instruction) - core dumped
Illegal instruction (core dumped)

then comment out the libarmmem line in ld.so.preload:

root@x4:~# cat pi/chroot/etc/ld.so.preload
#/usr/lib/arm-linux-gnueabihf/libarmmem.so

Install the things:

apt update
apt install busybox cryptsetup dropbear

To create an initramfs image we we need the kernel version. In my case
it is 4.4.50-v7+.

root@x4:/# ls -l /lib/modules/
total 8
drwxr-xr-x 3 root root 4096 Mar 11 20:31 4.4.50+
drwxr-xr-x 3 root root 4096 Mar 11 20:31 4.4.50-v7+

Create the image, enable ssh, and set the root password:

root@x4:/# mkinitramfs -o /boot/initramfs.gz 4.4.50-v7+
root@x4:/# update-rc.d ssh enable
root@x4:/# passwd

Set the boot command line. Previously I had:

root@x4:/# cat /boot/cmdline.txt
dwc_otg.lpm_enable=0 console=serial0,115200 console=tty1 root=/dev/mmcblk0p2 rootfstype=ext4 elevator=deadline fsck.repair=yes rootwait

The new one refers to the encrypted partition:

dwc_otg.lpm_enable=0 console=serial0,115200 console=tty1 root=/dev/mapper/crypt_sdcard cryptdevice=/dev/mmcblk0p2:crypt_sdcard rootfstype=ext4 elevator=deadline fsck.repair=yes rootwait

Add this to the boot config:

echo "initramfs initramfs.gz 0x00f00000" >> /boot/config.txt

Cat the private key and copy to the laptop; save as pikey:

root@x4:/# cat /etc/initramfs-tools/root/.ssh/id_rsa

The Offensive Security guide talks about editing /etc/initramfs-tools/root/.ssh/authorized_keys so that the ssh login can only run /scripts/local-top/cryptroot. I had no luck getting this to work, running into weird issues with Plymouth. For some reason the password prompt appeared on the physical console of the Pi, not the ssh session. So I skipped this and manually use the dropbear session to enter the encryption passphrase.

Set /etc/fstab to point to the new root partition. Original file:

root@x4:/# cat /etc/fstab
proc            /proc           proc    defaults          0       0
/dev/mmcblk0p1  /boot           vfat    defaults          0       2
/dev/mmcblk0p2  /               ext4    defaults,noatime  0       1
# a swapfile is not a swap partition, no line here
#   use  dphys-swapfile swap[on|off]  for that

New file (only one line changed, referring to /dev/mapper):

root@x4:/# cat /etc/fstab
proc            /proc           proc    defaults          0       0
/dev/mmcblk0p1  /boot           vfat    defaults          0       2
/dev/mapper/crypt_sdcard /               ext4    defaults,noatime  0       1
# a swapfile is not a swap partition, no line here
#   use  dphys-swapfile swap[on|off]  for that

Edit /etc/crypttab to look like this:

root@x4:/# cat /etc/crypttab
# 				
crypt_sdcard /dev/mmcblk0p2 none luks

The Offensive Security guide mentions that there can be issues with ports taking a while to wake up, so they recommend adding a 5 second sleep before the configure_networking line in /usr/share/initramfs-tools/scripts/init-premount/dropbear:

echo "Waiting 5 seconds for USB to wake"
sleep 5
configure_networking &

Regenerate the image:

root@x4:/# mkinitramfs -o /boot/initramfs.gz 4.4.50-v7+
device-mapper: table ioctl on crypt_sdcard failed: No such device or address
Command failed
cryptsetup: WARNING: failed to determine cipher modules to load for crypt_sdcard
Unsupported ioctl: cmd=0x5331

Now pop out of the chroot (Ctrl-D), unmount some things, and make a backup:

umount pi/chroot/boot
umount pi/chroot/sys
umount pi/chroot/proc
mkdir -p pi/backup
rsync -avh pi/chroot/* pi/backup/

umount pi/chroot/dev/pts
umount pi/chroot/dev
umount pi/chroot

Encrypt the partition, unlock it, and rsync the data back:

cryptsetup -v -y --cipher aes-cbc-essiv:sha256 --key-size 256 luksFormat /dev/mmcblk0p2
cryptsetup -v luksOpen /dev/mmcblk0p2 crypt_sdcard
mkfs.ext4 /dev/mapper/crypt_sdcard

mkdir -p pi/encrypted
mount /dev/mapper/crypt_sdcard pi/encrypted/
rsync -avh pi/backup/* pi/encrypted/

umount pi/encrypted/
cryptsetup luksClose /dev/mapper/crypt_sdcard
sync

Now put the sd card into the Pi and boot it up. If you see this on the console:

/scripts/local-top/cryptroot: line 1: /sbin/cryptsetup: not found

it means that the initramfs image didn’t include the cryptsetup binary. It is a known bug and the workaround that worked for me was:

echo "export CRYPTSETUP=y" >> /usr/share/initramfs-tools/conf-hooks.d/forcecryptsetup

(I had to do this in the chroot environment and rebuild the initramfs image. Ugh.)

For some reason I had Plymouth asking for the password on the physical console instead of the ssh dropbear connection. This is another known issue. This workaround looked promising but it broke the physical console as well as the ssh connection. No idea why.

What does work for me is to use the dropbear session to manually kill Plymouth and then enter the encryption password:

ssh -i pikey root@192.168.0.xxx

Then in the busybox session:

kill $(pidof plymouthd)
# Wait a few seconds...
echo -ne password > /lib/cryptsetup/passfifo
/scripts/local-top/cryptroot

This lets you enter the encryption passphrase. After a few seconds the normal boot process continues. So you can enter the encryption passphrase with a real keyboard if you are physically with the Pi, or you can ssh in if you are remote.