Unification & Substitution

Question

In Haskell, I have defined a polymorphic data type Subst a with a single constructor S :: [(String, a)] -> Subst a as so:

data Subst a where
    S :: [(String, a)] -> Subst a
    deriving (Show)

I want to define a function get::String -> Subst a -> Maybe a that takes a variable name and a substitution, and returns the value for which that variable must be substituted. If the substitution is not defined on the variable, the function should return Nothing.

I've tried the following:

get :: String -> Subst a -> Maybe a
get str (S[]) = Nothing
get str (S((a,b):xs)) = if str == a then Just b
    else get str xs

But I'm getting errors. Any ideas why?

Do you have any reason for using the GADT syntax? Couldn't you write your type more easily as data Subst a = S [(String, a)] deriving Show? — Tikhon Jelvis
@Tikhon no reason in particular actually, I was trying both ways as a learning mechanism to see if its different — NuNu
I'd suggest to use Map String a instead of [(String,a)]. Lookups for lists take O(n) while lookups for maps take O(log n). — Petr
+1 for @PetrPudlák suggestion. Even if you don't care about performance, the Map a b type has a very rich API for lookups and insertions. — Paul R

Daniel Fischer Daniel Fischer · Accepted Answer · 2012-11-07T03:01:15

get str (S((a,b):xs)) = if str == a then Just b
    else get str xs

xs is a list of type [(String, a)], but the second argument of get must be a Subst a. It would work if you used a constructor to construct a value of the correct type,

get str (S((a,b):xs)) = if str == a then Just b
    else get str (S xs)

but it is simpler to use the list directly to look up the variable,

Prelude> :t lookup
lookup :: Eq a => a -> [(a, b)] -> Maybe b

so

get str (S xs) = lookup str xs

does exactly what you want.

Unification & Substitution

1 Answers