A case for Dependent Types

dependent-types-using-gadts-and-datakinds.hs

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}

-- Support for https://nunoalexandre.com/2018/01/28/a-case-for-dependent-types


data ValueType = StringType | IntType

data Value :: ValueType -> * where
  StringValue :: String -> Value 'StringType
  IntValue :: Int -> Value 'IntType
 
resetWithDefault :: Value a -> Value a
resetWithDefault (StringValue _) = StringValue "Hello, world!"
resetWithDefault (IntValue _) = IntValue 3
 
serious :: Value 'StringType -> Value 'StringType
serious (StringValue str) = StringValue $ str ++ "!"

foo :: Value 'StringType -> Value 'IntType
foo (StringValue _) = IntValue 3

bar :: Value a -> Value a
-- Compiling error as 'IntValue' does not match 'StringValue'
bar (StringValue str) = IntValue 3