proj-oot-old-150618-principalTypesConsideredHarmful

example from http://en.wikibooks.org/wiki/Haskell/GADT

{-#LANGUAGE GADTs, EmptyDataDecls? #-} -- (the EmptyDataDecls? pragma must also appear at the very top of the module, -- in order to allow the Empty and NonEmpty? datatype declarations.)

data Empty data NonEmpty?

data SafeList? a b where Nil :: SafeList? a Empty Cons:: a -> SafeList? a b -> SafeList? a NonEmpty?

safeHead :: SafeList? a NonEmpty? -> a safeHead (Cons x _) = x

silly 0 = Nil silly 1 = Cons 1 Nil

Couldn't match `Empty' against `NonEmpty?' Expected type: SafeList? a Empty Inferred type: SafeList? a NonEmpty? In the application `Cons 1 Nil' In the definition of `silly': silly 1 = Cons 1 Nil

the recommendation is to do instead:

{-#LANGUAGE GADTs, EmptyDataDecls?, KindSignatures? #-} -- here we add the KindSignatures? pragma, -- which makes the GADT declaration a bit more elegant.

data NotSafe? data Safe

data MarkedList? :: * -> * -> * where Nil :: MarkedList? t NotSafe? Cons :: a -> MarkedList? a b -> MarkedList? a c

safeHead :: MarkedList? a Safe -> a safeHead (Cons x _) = x

-- this function will never produce anything that can be consumed by safeHead, since -- we have silly :: MarkedList? () NotSafe? silly 0 = Nil silly 1 = Cons () Nil silly n = Cons () $ silly (n-1)

however this would be unnecessary without principal types; without principal types, the compiler could just say, "silly might be "SafeList? a Empty" or it might be "SafeList? a NonEmpty?", i'm not sure which though"

---

why do ppl like principal types? i think it has to do with modularity. Probably b/c you can forget about a modules during type checking once you have its principal types. with the system i am proposing this would not be possible. another module interacting with yours might want to check some property that wasn't even defined when your module was written, like verifying that a value it passes is treated as a 'unique', e.g., never aliased.

i guess you can do something close, though; once you know all of the properties in the entire program, you can check each value for each property and remember that. But that sounds way inefficient in its own way (b/c presumably you don't need to know all those properties for most of the values).

https://www.google.com/search?client=ubuntu&channel=fs&q=%22beyond+principal+types%22&ie=utf-8&oe=utf-8#bav=on.2,or.r_cp.r_qf.&channel=fs&fp=fd10bb01e87334&q=Hindley-Milner++%22principal+types%22

i guess a compromise is to revert to (disjunctions of) principal-ish types at module boundaries. this isnt as restrictive as it seems, recalling that in Oot you can type annotate someone else's code, e.g. you can add that 'unique' qualifier that they didn't put there. This would work like a contract (assumption).