CODEWITHSUNDEEP
haskelldependent-type
MaiaVictor
MaiaVictor

Reputation: 52957

How to create a well-typed function that returns two different types?

I'm highly interested in compiling Formality-Core modules to Haskell libraries. While I could use unsafeCoerce everywhere, it would be more interesting if I could preserve the type information, allowing compiled modules to be published on Cabal and used by other Haskell projects. The problem is that dependent types allow programs that are forbidden by Haskell. For example, the function foo below:

foo: (b : Bool) -> If(b)(Nat)(Bool)
  (b)
  b<(b) If(b)(Nat)(Bool)>
  | zero;
  | false;

Returns a different type depending on the input. If the input is false, it returns the number zero. If the input is true, it returns the boolean false. It seems like a function like this can't be translated to Haskell. I believe that, on the last years, Haskell has made good progress towards dependent type, so, I wonder: is there any way to write functions that return different types based on the input value?

Upvotes: 3

Views: 270

Answers (3)

K. A. Buhr
K. A. Buhr

Reputation: 50819

It's maybe worth noting that, as a practical matter, the singletons library can be used to take care of most of the boilerplate. So, you can write:

{-# LANGUAGE GADTs #-}

module Formality where

import Numeric.Natural
import Data.Singletons.Prelude

foo :: SBool b -> If b Bool Natural
foo SFalse = 0
foo STrue = False

using almost exactly the syntax used by @dfeuer, up to the order of arguments to If.

The main disadvantage of the singletons library is that any serious type dependent programming is going to eventually require understanding how things are actually implemented internally, and the guts of the library are complicated and not very well documented.

You may find it helpful to start by hand-compiling some Formality using a from-scratch solution using your own singleton GADTs and type families (as in the other answers), and then try to convert it over to use singletons.

Upvotes: 3

dfeuer
dfeuer

Reputation: 48581

The state of the art remains the singleton approach.

data SBool b where
  SFalse :: SBool 'False
  STrue :: SBool 'True

type family If (b :: Bool) (t1 :: k) (t2 :: k) :: k where
  If 'False x _ = x
  If 'True _ y = y

foo :: SBool b -> If b Natural Bool
foo SFalse = 0
foo STrue = False

Upvotes: 6

Daniel Wagner
Daniel Wagner

Reputation: 152707

GADTs + TypeFamilies (optionally, + DataKinds) can do roughly this. So:

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

data GADTBool a where
    GADTFalse :: GADTBool False
    GADTTrue :: GADTBool True

type family If cond t f where
    If False t f = f
    If True  t f = t

foo :: GADTBool b -> If b Int Bool
foo GADTTrue = 0
foo GADTFalse = False

Of course, you'll probably actually want foo :: GADTBool b -> If b (GADTInt 0) (GADTBool False) if you plan to do this kind of thing pervasively. The search term you want for seeing more examples of this kind of hackery is "singleton types", often abbreviated just "singletons".

Upvotes: 6

Related Questions