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)
go
is factored into forth
and back
with intermediary types dependent on Simple
should be preserved.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