Search code examples
haskelldependent-type

How to avoid repetition when "factoring" a Haskell function into two functions with various intermediary types?


Consider the following Haskell code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}

import Data.Singletons.TH

singletons [d| data SimpleType = Aaa | Bbb | Ccc | Ddd
                                 deriving (Read)
             |]

-- each SimpleType value has an associated type
type family Parsed (t :: SimpleType) :: * where
  Parsed Aaa = [Int]
  Parsed Bbb = Maybe Int
  Parsed Ccc = (Int, Int)
  Parsed Ddd = Int

forth :: SSimpleType t -> Int -> Parsed t
forth SAaa x = [x,x*2,x*3]
forth SBbb x = Just x
forth SCcc x = (1337, x)
forth SDdd x = x

back :: SSimpleType t -> Parsed t -> Int
back SAaa [_, y, _] = y + 5
back SBbb (Just y) = y - 7
back SCcc (y1, y2) = y1 + y2
back SDdd y = y * 2

helper b = back b . forth b

go :: SimpleType -> Int -> Int
go Aaa = helper SAaa
go Bbb = helper SBbb
go Ccc = helper SCcc
go Ddd = helper SDdd

main = do
  -- SimpleType value comes at run-time
  val <- readLn
  putStrLn $ show $ go val 100

Is it possible to avoid the repetition when go is defined? In other words, is there a way to write something like:

go val = helper (someMagicFunction val)
  • singletons do not have to be a part of the solution,
  • ... but the idea that go is factored into forth and back with intermediary types dependent on Simple should be preserved.

Solution

  • You can use toSing from SingKind to convert a value of SimpelType to a value of SomeSing SimpleType, which is an existentially quantified wrapper around Sing SimpleType. You can then unwrap that value to get Sing SimpleType, which you can then pass to back and forth:

    go :: SimpleType -> Int -> Int
    go val x =
      case toSing val of
        SomeSing s -> back s $ forth s x
    

    An instance of SingKind is generated for you (among many other things) by the singletons splice that you're using.

    Note that, while a single-branch case is asking to be a let, this wouldn't compile:

    go val x =
      let (SomeSing s) = toSing val
      in back s $ forth s x
    

    This is prohibited, because let can be recursive, and since unwrapping a GADT may bring new types into context, it may result in creating an infinite type. A case branch, on the other hand, cannot be recursive, so this works. (credit for this explanation to @HTNW)

    But a helper function would also work:

    go val x = helper $ toSing val
        where
          helper (SomeSing s) = back s $ forth s x